merged

misc tuning and clarification;

more compact representation;

more compact representation of theory_id -- via consecutive thread-local ids;

more compact representation;

tuned signature;

more compact representation of theory_id;

tuned signature;

compact representation of sets of integers;

more reactive headless server, in contrast to 15656ad28691 (when "isabelle…

tuned whitespace;

clarified modules;

clarified signature;

clarified modules;

clarified modules: Build_Log.private_data provides raw data access without…

more thorough transaction_lock;

obsolete, see also a5896fe040dd;

removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);

provide src/Tools/Demo as example for system component with Isabelle/Scala tool;

merged

clarified buffer_size;

more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);

merged

disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL…

workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read…

tuned;

prefer Unix-domain socket on Unix;

support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;

tuned;

clarified signature: more general make_streams;

tuned;

more robust exception handling (amending 8cc1ae43e12e);

clarified signature: avoid deprecated URL constructors;

avoid deprecated URL constructors;

proper build with jdk-21 (amending 4fb5e6499da9);

more realistic timeouts for lrzcloud2:threads=1;

NEWS;

update to jdk-21.0.1;

rebuild jedit with minimal patch for jdk-21, following SVN 25690;

clarified modules;

suppress duplicate entries systematically using log_name: e.g. relevant for AFP;

clarified operation: pick current pull_date instead of previous one;

build_history: proper support for ISABELLE_APPLE_PLATFORM64;

prefer symbolic build_history_base_arm;

clarified isabelle_hg (again, see b9d59669904a);

clarified signature: explicit Remote_Build.count instead of duplicate entries…

clarified signature: more operations and options concerning Isabelle hg;

performance tuning: cache graph;

unused (see also 004b39bf06a5);

tuned signature: fewer warnings in IntelliJ IDEA;

clarified signature and modules: more explicit Build_Log.History;

tuned: avoid recursion;

tuned;

avoid duplicate data;

output more data;

clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;

tuned whitespace;

proper ml_statistics (amending aeb511a520f4);

tuned signature;

merged

tuned signature;

clarified signature: more operations, allow recursive get;

support for "cluster" table with "hosts" array, and params/options as for…

tuned signature: more operations;

clarified signature;

tuned output;

more robust: prefer strict operations;

tuned message;

tuned signature: more operations;

proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in…

clarified signature;

clarified modules;

clarified signature: more operations;

prefer strict test of system options;

more NEWS;

more TODO;

tuned comments;

some build cluster resources at TUM;

more robust init;

build cluster host specifications are based on registry entries (table prefix…

support interpreted/typed entries via Registry.Category and Registry.Table;

clarified signature: more operations;

clarified output;

clarified signature: more operations;

support for global registry;

clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require…

clarified signature: emphasize mutable instance;

clarified signature: more operations;

support for explicit SSH hostname;

proper local host (amending 62d7ef1da441);

proper default for disjunction (amending 9f7a94117666);

tuned;

more operations;

avoid option -C: free this latter for build-related configuration;

more direct indentation, using Symbol.spaces;

more accurate treatment of surrounding whitespace;

clarified signature;

obsolete (see also f627ab8c276c);

tuned signature;