src/Pure/System/progress.scala
Thu, 02 Nov 2023 11:57:40 +0100 wenzelm clarified signature: explicit Progress date;
Thu, 02 Nov 2023 10:23:28 +0100 wenzelm more robust: support concurrent output;
Tue, 29 Aug 2023 17:40:01 +0200 wenzelm clarified signature: prefer enum types;
Sun, 27 Aug 2023 14:22:28 +0200 wenzelm more robust access to local variables;
Tue, 22 Aug 2023 12:18:31 +0200 wenzelm proper sync_database for receive timeout;
Tue, 22 Aug 2023 11:54:06 +0200 wenzelm clarified source structure;
Mon, 21 Aug 2023 15:04:22 +0200 wenzelm clarified signature: proper treatment of implicit state (amending d0c9d277620e);
Mon, 21 Aug 2023 12:34:53 +0200 wenzelm clarified signature: more robust treatment of implicit state;
Mon, 21 Aug 2023 11:56:07 +0200 wenzelm proper sync_database for Database_Progress consumer;
Mon, 21 Aug 2023 11:43:29 +0200 wenzelm tuned message;
Mon, 21 Aug 2023 11:42:16 +0200 wenzelm tuned;
Sun, 20 Aug 2023 22:24:24 +0200 wenzelm limit size and complexity of bulk transactions;
Sat, 19 Aug 2023 22:57:06 +0200 wenzelm clarified signature: filter batch;
Sat, 19 Aug 2023 14:45:57 +0200 wenzelm more scalable write_messages via db.execute_batch_statement;
Thu, 17 Aug 2023 20:13:49 +0200 wenzelm more robust;
Thu, 17 Aug 2023 20:06:24 +0200 wenzelm restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
Thu, 17 Aug 2023 19:01:40 +0200 wenzelm more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
Thu, 17 Aug 2023 14:46:24 +0200 wenzelm clarified signature;
Wed, 16 Aug 2023 14:42:43 +0200 wenzelm build_worker is stopped independently from master build_process;
Thu, 10 Aug 2023 16:57:01 +0200 wenzelm more robust;
Thu, 10 Aug 2023 16:49:17 +0200 wenzelm tuned signature;
Thu, 10 Aug 2023 16:40:07 +0200 wenzelm clarified signature: more explicit types;
Sat, 22 Jul 2023 12:10:03 +0200 wenzelm tuned signature;
Tue, 18 Jul 2023 19:51:12 +0200 wenzelm renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
Tue, 18 Jul 2023 12:19:12 +0200 wenzelm clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
Mon, 17 Jul 2023 20:31:45 +0200 wenzelm clarified errors;
Sun, 16 Jul 2023 11:29:23 +0200 wenzelm more informative trace;
Sat, 08 Jul 2023 13:13:10 +0200 wenzelm clarified signature;
Fri, 07 Jul 2023 14:17:53 +0200 wenzelm clarified signature;
Sun, 02 Jul 2023 20:09:12 +0200 wenzelm more robust "stop": further "stamp" ticks may happen afterwards;
less more (0) -50 -30 tip