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 = {}