clarified signature;

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;