proper Build_Cluster.Host.parse for parameters and system options; clarified Build_Cluster.Host: empty "host" means local;

more operations for independent "inline" options;

clarified options: accommodate potentially slow database connection;

minor performance tuning;

add option "build_context" in anticipation of AFP entries that require special tricks in Isabelle/ML (NB: system component settings are unavailable in AFP);

proper build_options (amending 822ddccda899);

clarified options;

proforma support for remote build hosts;

more options for performance tuning;

more operations;

support for management of build cluster;

clarified modules;

renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);

more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh;

proper running limit, based on this worker process; prefer bulk jobs: much faster cancellation;

more robust: implicit locking of tables in standard order;

more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked;

removed unused "create_index": implicit index from primary_key is usually sufficient;

clarified "vacuum" (again, reverting 0bd366fad888);

clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);

update for release;

merged

more elementary transaction implementation (despite fda3f7a158b9 and 9da65bc75610);

tuned signature;

proper check (amending 234f2ff9afe6);

more robust: exclude accidental nesting (synchronized block is re-entrant);

clarified errors;

removed junk (amending f8e3b228670c);

tuned output;

reuse SSH.Server connection for database server;

tuned source structure;

clarified check: uniform session_info_exists;

more complete check;

clarified signature: more specific exists_table --- avoid retrieving full list beforehand;

reuse database_server connection;

more informative trace;

reuse SSH.Server connection database server;

tuned output;

make double-sure that this is a transaction context, notably for LOCK TABLE;

more robust Java/Scala multithreading: transaction is always connection.synchronized;

clarified signature: proper Scala function for command-line tool;

tuned signature;

clarified signature: more operations;

more standard time unit;

clarified options;

tuned output;

global transaction_count;

tuned output;

tuned output;

prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job");

clarified isabelle.transaction_log: support time_min (in ms);

more operations;

more informative trace;

support trace of transaction_lock via property "isabelle.transaction_log";

proper db.transaction_lock instead of adhoc clone (amending 2df0f3604a67);

tuned;

proper close() operation;

tuned comments;

more robust: avoid nested transactions (on disjoint tables);

potentially more robust: long-running operation only for build master, not workers;

less ambitions transactions (amending 3f3dcf9f53f1): TRANSACTION_SERIALIZABLE may lead to spurious rollback exceptions;

clarified signature: more operations;

clarified signature: more operations;

clarified signature;

clarified signature;

clarified signature: follow Store.open_database;

tuned;

clarified signature;

clarified signature: more uniform SSH.Port_Forwarding;

tuned signature;

X = trivial_topology rather than topspace X = {}

merged

trivial_topology

merged;

added docs for order method in Orderings; The order method is now tried by try0. This adds some documentation for users of try0 that stumble over the order method

News update referring to Analysis

tuned error message;

more NEWS;

tuned output;

tuned output;

clarified session_statistics: removed somewhat pointless per-theory statistics;

tuned error messages;

more TOML formatting functions;

merged

Doubled the time limit for HOL-Probability

merged

Some fixes, and SOME TIME LIMITS

merged

cosmetic improvements, new lemmas, especially more uses of function space

more NEWS;

NEWS;

tuned whitespace;

added TOML module from afp;

proper system integration and renaming;

copy/rename files from private autocorres version e45b9b680d3e;

Added tag Isabelle2023-RC1 for changeset 006dbc9c2de1