actually executable enum_all, enum_ex for word

tuned text

Lots of new material chiefly about complex analysis

merged

More new theorems from the number theory development

merged

proper orientation for right-associative operations;

tuned signature;

tuned signature;

tuned signature;

obsolete --- superseded by SHA1.Shasum operations;

clarified signature, using right-associative operation;

tuned whitespace;

tuned --- implicit split;

clarified signature;

prefer explicit shasum: more robust due to explicit file names, which often work implicitly in LaTeX;

tuned signature;

more uniform use of SHA1.Shasum;

proper Shasum.digest, to emulate old form from build_history database; clarified signature: more explicit types;

prefer explicit shasum; clarified signature;

proper symbolic dependencies, e.g. for Demo_FoilTeX;

prefer explicit shasum;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature;

Some more new material and some tidying of existing proofs

more diagnostic operations (see also 5c7652e9bc01);

more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);

clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);

tuned;

clarified modules;

tuned signature;

update to polyml-5e9c8155ea96, which is more robust on arm64;

more robust dependencies for Pure;

proper compiler root for arm64;

clarified "isabelle build_polyml": download and build everything for current platform; renamed former "isabelle build_polyml" to "isabelle make_poly", for experimentation and diagnosis;

no view_document after build: avoid loss of focus, especially in "auto build" mode;

tuned message;

build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;

clarified modules;

maintain document_output meta data;

clarified modules;

avoid redundant SelectionChanged events;

more logging;

proper symbolic handle on component resources: diff -r ci-extras-1/etc/settings ci-extras-2/etc/settings 1c1,4 < classpath "$COMPONENT/lib/ci-extras.jar" --- > #-*- shell-script -*- :mode=shellscript: > > ISABELLE_CI_EXTRAS_JAR="$COMPONENT/lib/ci-extras.jar" > classpath "$ISABELLE_CI_EXTRAS_JAR" diff -r ci-extras-1/README ci-extras-2/README 11a12 > Makarius, 02-Feb-2023

more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);

More of Manuel's material, and some changes

less verbosity by default, notably for regular "isabelle build -o document";

clarified message: old-style log is usually empty;

clarified messages, notably for session "Intro";

merged

more general program start message; progress on "Creating directory";

clarified terminology of inlined "PROGRAM START" messages;

isabelle update -u cite -l "";

less ambitious parallelism: avoid exhaustion of memory (40GB total);

clarified GUI;

clarified GUI: omit pointless search buttons, as real output is shown as markup;

more uniform use of Symbol.output, even in situations where its Symbol.encode is usually redundant;

merged

More new material thanks to Manuel

merged

tuning

alternate AFP tests on lrzcloud2, to fit better into one day;

merged

support document preparation from already loaded theories;

clarified GUI events;

clarified GUIs: keep related buttons together;

proper program name, e.g. for session "Intro";

clarified GUI events: reset everything on session context switch;

clarified GUI events: ensure fresh output when switching pages;

clarified GUI: avoid odd jumping pages on "Cancel";

clarified GUI events;

more accurate output: avoid output_body from last run;

more accurate output: avoid output_main from last run;

removed unused operation from 3f50b24909df;

clarified guard: avoid spurious auto builds;

automatically build document when selected theories are finished;

more accurate Word.capitalize: do not touch name;

defer build until document nodes are ready;

clarified signature: prefer semantic status;

removed obsolete parameter (see 7c23db6b857b);

clarified Document_Editor.Session: more explicit types, more robust operations; eliminated await_stable_snapshot in favour of delay_build;

more operations;

clarified operation (without change of signature!);

pointless

Lots more new material thanks to Manuel Eberl

merged

Moved in a large number of highly useful library lemmas, mostly due to Manuel Eberl

observe option "show_states" in headless server (see also 951abf9db857);

text correction

enable clean_components by default: it saves a lot of local disk space, notably on virtual nodes;

merged

removed somewhat pointless support for Jenkins log files: it has stopped working long ago;

more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";

tuned signature;

more operations;

obsolete (see also d547173212d2);

clarified names to emphasize suble differences in meaning;

prefer high-level Other_Isabelle.bash over low-level SSH.execute;

unused (see 378bb7a739c3);

more options to manage resolved components;

proper use of current ISABELLE_COMPONENT_REPOSITORY from the managing Isabelle system (amending 3e963d68d394);

tuned comments;

tuned;

clarified signature: more explicit types; scale chart output, instead of stored data;

more operations;

tuned;

clarified signature: more robust field_scale;

clarified signature: more explicit types;

clarified signature;

tuned;

support units, e.g. java.lang.Long.MAX_VALUE is 8 EiB;

more explicit types;

prefer typed/strict operations;

tuned message;

prefer strict operation: java.io.File.length returns 0 for non-existent file;

prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;

back to Scala 3.2.0 for now, since 3.2.1 causes odd crash of REPL concerning value classes (e.g. "isabelle.Time.now()"); enforce rebuild of Isabelle/ML + Isabelle/Scala;

Restored antiquotation.

tuned whitespace