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)
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: Nov 21 2024 at 12:39 UTC