src/Pure/System/progress.scala
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;
Sun, 02 Jul 2023 18:56:52 +0200 wenzelm clarified signature;
Sun, 02 Jul 2023 15:25:12 +0200 wenzelm more SQL data;
Wed, 21 Jun 2023 14:27:51 +0200 wenzelm clarified signature: more explicit class SQL.Data;
Fri, 16 Jun 2023 14:20:18 +0200 wenzelm proper support for SQLite: avoid conflicts on transaction_lock;
Wed, 14 Jun 2023 16:27:44 +0200 wenzelm prefer Database_Progress, which is more robust (amending afb1a19307c4);
Wed, 14 Jun 2023 15:37:30 +0200 wenzelm support for Database_Progress;
Sun, 05 Mar 2023 18:38:52 +0100 wenzelm more robust: disallow override;
Sat, 04 Mar 2023 22:29:21 +0100 wenzelm clarified treatment of "verbose" messages, e.g. Progress.theory();
Sat, 04 Mar 2023 21:25:12 +0100 wenzelm tuned whitespace;
Sat, 04 Mar 2023 17:36:29 +0100 wenzelm more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
Sat, 04 Mar 2023 16:15:50 +0100 wenzelm tuned;
Sat, 04 Mar 2023 12:59:22 +0100 wenzelm tuned messages;
Sat, 04 Mar 2023 12:43:35 +0100 wenzelm clarified signature: require just one "override def echo(message: Progress.Message): Unit";
Sat, 04 Mar 2023 12:05:51 +0100 wenzelm clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
less more (0) -50 -30 tip