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;