proper afp_root;

clarified signature: more "object-oriented" style;

more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process;

clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;

tuned signature;

tuned signature; more operations;

clarified option (see also b66b6cc1eb8c);

more build_cluster management: open SSH connections in parallel, but synchronously;

tuned signature: more options;

clarified signature: more operations;

tuned signature;

more accurate print vs. parse;

clarified signature; tuned output;

clarified signature (again); more explicit "local" name;

tuned output;

tuned output;

clarified modules;

more pro-forma support for afp_root;

tuned NEWS: emphasize "isabelle build" add-ons;

added option -A for AFP root, following "isabelle sync";

clarified signature: more operations;

tuned signature;

clarified file location: to be used by regular Isabelle/Scala tools;

update headers;

more pro-forma support for Build_Cluster;

tuned;

tuned;

clarified options;

clarified options;

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;