Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Folding pretty-printed output by default

view this post on Zulip Email Gateway (May 06 2024 at 05:35):

From: hannobecker@posteo.de
Hi,

Pretty.text_fold creates foldable pretty printing output. By default,
the output seems to be unfolded.

Is it possible to refine Pretty.text_fold so one can specify whether
the output should initially be unfolded or folded?

I would like to print high-level information in the output buffer and
allow the user to selectively unfold further details. Printing all
details by default is inscrutable in my application.

Thanks!
Hanno

Last updated: May 19 2024 at 04:18 UTC