merged

merged

clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);

clarified signature;

tuned GUI: avoid wasting space with proportional fonts;

clarified signature;

more accurate pretty_margin for proportional fonts;

clarified signature: more uniform;

tuned: fewer warnings in IntelliJ IDEA;

tuned signature;

tuned signature;

clarified signature with subtle change of semantics: output consists of individual messages that are formatted (and separated) internally;

more accurate message boundaries;

tuned whitespace;

clarified signature: more robust type XML.Elem;

clarified signature;

clarified signature;

clarified output representation: postpone Pretty.separate;

tuned;

tuned: fewer warnings in IntelliJ IDEA;

clarified signature: more accurate types;

tuned signature: more standard names;

more uniform pretty_text_area.zoom via its zoom_component;

tuned signature;

tuned signature: more standard names;

tuned;

clarified signature;

clarified signature;

tuned;

revert 1206400b9b48: proper Node.unapply for Node.apply(null);

tuned signature;

clarified signature;

clarified signature, with subtle change of semantics: proper non-null result;

clarified modules;

more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956);

misc tuning;

try0: avoid mapping background theory -- should be handled by Context_Position visibility;

try0: stop early if more subgoals are created;

try0: filter out untagged thms;

try0: support literal facts;

try0: add 'use' modifier for thms to insert;

try0: use extra thms via insert;

clarified: proper type for facts;

clarified: proper type;

tuned;

tuned;

try0: pass tagged thms for better control;

clarified: proper return type;

improve try0: solve multiple subgoals at once, if possible;

tuned: unused parameter;

tuned

better termination behaviour

uniform name T_f for closed-form lemmas for function T_f

More time for primitive functions

merged Reverse into Time_Funs

tuned proofs;

tuned description: plain text documentation is also supported;

merged

update to jdk-21.0.5; enforce rebuild of Isabelle/ML and Isabelle/Scala;

misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; recover plain file support from 488c7e8923b2;