added field input_eqns to record the list of equations (the specification) given to the function command.

merged

more NEWS;

tuned proofs;

more ambitious mouse handler: double-click selects highlight_area;

more accurate mouse handler: only for single clicks, consume accepted event;

more ambitious scrolling: retain original scroll position if possible;

more ambitious scrolling: retain bottom position after output;

performance tuning: cache for Rich_Text.format, notably for incremental tracing;

clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;

omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;

tuned;

minor performance tuning: avoid duplication of Symbol.spaces (e.g. from Pretty.formatted);

clarified signature and modules; more basic Rich_Text.formatted_lines, assuming that elements are properly separated according to Rich_Text.format;

performance tuning for macOS (after update of "jedit" component): old OpenGL works better for text rendering;

performance tuning: more incremental update of buffer content;

obsolete;

clarified: more uniform results;

clarified signature: inline org.gjt.sp.jedit.textarea.TextArea.setText();

minor performance tuning: avoid concatenation of existing string material;

clarified signature and data storage: incremental lazy values;

tuned comments;

clarified signature;

clarified modules;

clarified margin operations (again, reverting 4794576828df);

clarified modules;

more reactive interrupts (via Future.cancel);

Document.Snapshot: support for multiple snippet_commands; clarified Command.rich_text: prefer explicit id, e.g. from message serial; clarified Pretty_Text_Area.update: Protocol_Message.provide_serial; clarified Pretty_Text_Area.format_rich_texts, with separate formatting of messages;

more robust: make double-sure that this is the correct output, not a different version from concurrent GUI_Thread.later;

clarified signature: include standard margin in object equality;

performance tuning: prefer asynchronous Pretty.formatted, which actually takes longer than Command.rich_text (see also 97964515a676, where Pretty.formatted was on the GUI thread, maybe for the sake of java.awt.FontMetrics at that time);

The ceillog2 function (thanks to Manuel Eberl), replacing two copies of Ceil_Log2

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;

tuned proofs

added missing definitions

tuned proofs; more Isabelle symbols;

clarified modules;

support value-oriented Font_Metric, e.g. for caching Pretty output;

tuned;

unused;

tuned;

tuned;

clarified signature; clarified modules;

more accurate Symbol.Metric, following 6eccae338770;

tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);

proper parentheses, for the sake of IntelliJ IDEA;

clarified modules;

clarified signature;

tuned proofs;

tuned GUI (again, see 0521e65af41e);

tuned proofs;

tuned;

tuned comments;

clarified signature;

tuned;

tuned names;

more robust;

clarified signature;

unused;

clarified signature: more explicit types;

tuned GUI;