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;

clarified names;

clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;

clarified modules;

clarified modules;

tuned;

clarified signature: avoid dispatch via name;

clarified, e.g. type variables;

tuned index;

more ambitious default for index "is like";

tuned;

support for index entries;

tuned;

tuned signature;

clarified modules;

clarified old document build;

unused;

prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee;

prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document;

unused;

proper Unix lines;

prefer explicit option document_bibliography (actually ignored by build script);

explicit option document_bibliography;

proper bibliography;

discontinued obsolete "isabelle latex";

more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; clarified ISABELLE_MAKEINDEX options;

default document_build (lualatex);

more robust: allow \printindex within the document;

clarified bash scripts, with public interfaces for user-defined Document_Build.Engine;

tuned signature;

option document_preprocessor;

show symbols in Isabelle/ML instead of perl;

more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;

tuned --- more robust;

discontinued somewhat pointless "fixbookmarks": default output works sufficiently well;

more uniform bibtex error, without using perl (see 4710dd5093a3);

proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error);

tuned;

clarified command-line options;

obsolete (see 5a3a2a52648d);

redundant: copy produced from session document_files;

clarified treatment of Isabelle .sty files;

option document_logo;

proper options;