Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Default print modes


view this post on Zulip Email Gateway (Aug 19 2022 at 13:09):

From: Peter Lammich <lammich@in.tum.de>
Hi all,

in Monad_Syntax, there is a print mode (do_notation).

How can I activate this print mode to be applied to all default output
of 1) PG 2) isabelle/jEdit. (Not sure if the above uses technical
correct terminology, so, simply speaking: I want to see do-notation
rather than >>= - syntax)

view this post on Zulip Email Gateway (Aug 19 2022 at 13:09):

From: Makarius <makarius@sketis.net>
The very ancient option -m is available for all of isabelle-process,
isabelle emacs, isabelle jedit.

The interface wrappers also allow persistent options within the settings
environment, using PROOFGENERAL_OPTIONS and ISABELLE_JEDIT_OPTIONS,
respectively.

Further hints in the "system" manual.

Makarius


Last updated: Apr 26 2024 at 16:20 UTC