prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;

clarified signature: more explicit operations;

tuned: trim message before formatting;

tuned signature: more operations;

clarified signature;

clarified print_mode (again, amending 9de19e3a7231): support e.g. 'thm ("") symmetric' for formatting in ML and without markup;

more robust reports: ensure that markup is actually present;

tuned signature;

clarified internal tool output: prefer Pretty.pure_string_of over manipulation of print_mode;

unused;

misc tuning and clarification (see also 86a31308a8e1);

tuned signature: more operations;

clarified modules;

dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";

clarified YXML bootstrap;

tuned;

more robust: global ML name space for markup elements;

clarified properties;

clarified signature and modules;

further clarification of print_mode: PIDE markup depends on "isabelle_process" alone, Latex is stateless;

misc tuning and clarification;

minor performance tuning, notably for Bytes.add (e.g. YXML output);

revert 90f6e541e926, which has become pointless thanks to df85df6315af;

clarified signature and modules;

clarified files;

drop pointless print_mode operations Output.output / Output.escape;

clarified signature: prefer explicit type Bytes.T;

clarified signature, roughly following Isabelle/Scala;

clarified print mode "latex": no longer impact Output/Markup/Pretty operations; renamed Output.output to Output.output_; removed Output.escape;

tuned comments, following Isabelle/ML;

tuned module structure;

tuned;

clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;

clarified signature;

tuned signature;

tuned;

minor performance tuning, following Isabelle/Scala;

tuned;

tuned signature;

more scalable;

tuned;

eliminate print mode "code_presentation" thanks to value-oriented Pretty.T operations;

NEWS: value-oriented Pretty.T;

proper formal sections;

tuned signature: more options;

clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree; clarified Pretty.symbolic: always use YXML.output_markup;

minor performance tuning;

unused;