clarified signature;

more NEWS;

tuned proofs;

merged

enforce rebuild of Isabelle/ML and Isabelle/Scala;

update to jedit-20241115 (see also ecd62f7b3644 and d92d754b5dd9);

more patches for the sake of SideKick 1.8 vs. jEdit 5.7.0: provide missing GUIUtilities.isPopupTrigger, avoid StatusBar messages (which often don't fit);

tuned comments;

clarified key events: cancel output selection, before input selection;

proper focus to support subsequent copy-paste via keyboard;

more accurate initial FontRenderContext, notably on macOS, Windows, or Linux with "env GDK_SCALE=2";

removed obsolete option: jEdit 5.7.0 can be built with default jdk;

more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);

less ambitious selection;

mv Discrete to Discrete_Cpo to avoid theory name clashes

disable 2d9b6e32632d for now: unknown problems on macOS;

clarified mouse selection, avoid conflict of double-click with single-click (follow hyperlink);

more careful isConsumed() / consume() for key and mouse events;

merged

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;