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;