proper Font_Subst.cache for paintScreenLineRange;

more predictable result, avoid slightly odd "lastSubstFont" by jEdit;

tuned;

tuned signature;

tuned;

discontinue i21of4 (old Apple hardware);

avoid deprecated operation;

tuned;

support for jEdit font substitution;

more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java); more direct TextAttribute.RUN_DIRECTION_LTR (see also ce22e5c3d4ce);

updated to flatlaf-1.2;

proper directories after reinstallation of lxbroy10;

more visual emphasis on node status;

more word cleanup

merged

more default simp rules

some word streamlining

avoid legacy domain informatik.tu-muenchen.de;

tuned --- following hints by IntelliJ;

tuned signature;

tuned;

tuned;

tuned signature;

tuned;

tuned signature (see 2d6a489adb01);

added support for TFX's and THF's $ite to Sledgehammer

tuned Mirabelle documentation

shortened long lines

fixed typos

updated Mirabelle documentation

changed Mirabelle's filter to use short theory names

more lemmas

added support for unbounded max calls to Mirabelle

added warnings when defining unamed or redefining Mirabelle action

tuned whitespace;

tuned Mirabelle

merged

refactored Mirabelle to produce output in real time

global interpretation into nested targets

more succint interfaces

merged

tuned messages;

NEWS;

proper profiling within command execution: messages require PIDE id;

more systematic treatment of profiling mode;

tuned message;

prefer less intrusive tracing message;

clarified documentation: tracing messages are not shown here;

add missing file;

more formal ML profiling messages;

clarified modules;

Lukas Steven's more general fold foctions for maps

More general fold function for maps

follow Phabricator update 2021 Week 23;

tuned;

more formal theory and session names; tuned whitespace;

proper NEWS after Isabelle2021;

updated descriptions;

allow system option short form NAME for NAME=true for type string, not just bool; support short system options "-o document" and "-o system_log";

tuned;

more robust within session "HOL";

merged

suppress theories from other sessions, unless explicitly specified via mirabelle_theories;

clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);

refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;

tuned;

more uniform schedule_theories, notably for "present" and "commit" phase after loading;

tuned;

moved more legacy to AFP

clarified modules;

clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);

tuned;

more thorough update of required files (amending 1529c3eb6bac);

clarified examples;

tuned proofs;

misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);

tuned --- reduced source complexity;

proper usage (amending f7ea394490f5);

merged, resolving minor conflict;

allow build session setup, e.g. for protocol handlers;

unused;

tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated);

clarified signature;

removed pointless option (see 3d0952893db8);

tuned --- avoid redundant future tasks from already loaded theories;

no comment --- topological order appears to be fine since 04-Mar-2013;

more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7);

moved stride option from sledgehammer action to main mirabelle

merged

new lemmas mostly about paths

lexorders the locale way

more accurate export morphism enables proper instantiation by interpretation

merged

some new and/or varient results about images

nicer statement of Liouville_theorem

more lemmas

max word moved to Word_Lib in AFP

more robust syntax;

unused;

clarified document export names;

tuned signature;

tuned;

tuned;

avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;

compose Latex text as XML, output exported YXML in Isabelle/Scala;

more direct index_entry: no positions required -- text is eventually moved to .ind file;

clarified signature;

clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");

tuned message, e.g. for Pure bootstrap;

proper signature export (amending b50f8cc8c08e);

syslog option for "isabelle build";

further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea);

merged

NEWS;

clarified index, more like formal @{element_ref};

clarified treatment of type constructors;

misc tuning and clarification;

tuned signature;

clarified context;

more uniform document antiquotations for ML: consolidate former setup for manuals;