[isabelle-dev] NEWS: Stateless pretty-printing without print_mode

[Makarius]

*** ML ***

* Constructors for type Pretty.T (such as Pretty.str, Pretty.mark_str,
Pretty.markup_block) are now value-oriented. Use of the global
print_mode is restricted to ultimate Pretty.string_of (and some
variants), while the underlying Pretty.output operation supports an
explicit Pretty.output_ops argument for alternative applications.

* Pretty.pure_output_ops and Pretty.pure_string_of support
pretty-printed output without PIDE markup. This is occasionally useful
for special tools, in contrast to regular user output. Manipulation of
the print_mode via (Print_Mode.setmp []) is no longer required.

* The print_mode "latex" only affects inner syntax variants, while its
impact on Output/Markup/Pretty operations has been removed. Thus the
print_mode operations Output.output and Output.escape have become
obsolete: superseded by Latex.output_ and Latex.escape specifically for
LaTeX. Rare INCOMPATIBILITY for ambitious document antiquotations that
generate Latex source on their own account, instead of using regular
Pretty.T interfaces (that are based on Latex.output_ops internally).
Note that basic Markup.markup cannot be used for Latex output: proper
Pretty.T operations are required (e.g. Pretty.mark_str).


This refers to Isabelle/e55723709fab.

I have reworked many ancient things substantially, often not very pretty. 
There is now also a change from type string to Bytes.T, which is not bounded 
by the 64MB limit. Thus very ambitious applications can pretty print huge 
messages without explicit limits --- it might still overwhelm the front-end.


	Makarius