[isabelle-dev] NEWS: show_markup

[Makarius]

* 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 
becoming real.

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.


 	Makarius