[isabelle-dev] NEWS: show_markup
makarius at sketis.net
Thu Oct 4 14:05:56 CEST 2012
* Configuration option show_markup controls direct inlining of markup
into the printed representation of formal entities --- notably type
and sort constraints. This enables Prover IDE users to retrieve that
information via tooltips in the output window, for example.
This refers to Isabelle/1301ed115729, which should mark the point in
history where life without manual setting of show_types/show_sorts is
The precise interaction of this new default option for Isabelle/jEdit with
several other options (show_types, show_sorts, show_consts,
show_all_types, ...) is not fully clear to me yet. At the moment,
explicit show_types/show_sorts revert to the old behaviour with (partial)
printing of constraints instead of (complete) markup, but a printed goal
state has further add-ons that are still ignored.
More information about the isabelle-dev