| Sat, 14 Jun 2025 14:31:54 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 01 Jun 2024 21:52:31 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 01 Jun 2024 21:49:50 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 01 Jun 2024 15:11:46 +0200 |
wenzelm |
support bash via SSH;
|
file |
diff |
annotate
|
| Sat, 01 Jun 2024 12:35:38 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 01 Jun 2024 12:31:06 +0200 |
wenzelm |
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
|
file |
diff |
annotate
|
| Wed, 13 Mar 2024 23:26:30 +0100 |
wenzelm |
revert most parts of 0e79fa88cab6: somewhat ambitious attempt to move towards "editing" builds via added/canceled workers;
|
file |
diff |
annotate
|
| Tue, 12 Mar 2024 15:57:25 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2024 10:50:12 +0100 |
wenzelm |
tuned signature: more uniform SQL.Data instances;
|
file |
diff |
annotate
|
| Mon, 04 Mar 2024 11:05:36 +0100 |
wenzelm |
more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b);
|
file |
diff |
annotate
|
| Sun, 25 Feb 2024 20:40:21 +0100 |
wenzelm |
database performance tuning: prefer light-weight IPC over heavy-duty transactions;
|
file |
diff |
annotate
|
| Sat, 24 Feb 2024 11:05:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 11:57:40 +0100 |
wenzelm |
clarified signature: explicit Progress date;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 10:23:28 +0100 |
wenzelm |
more robust: support concurrent output;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 17:40:01 +0200 |
wenzelm |
clarified signature: prefer enum types;
|
file |
diff |
annotate
|
| Sun, 27 Aug 2023 14:22:28 +0200 |
wenzelm |
more robust access to local variables;
|
file |
diff |
annotate
|
| Tue, 22 Aug 2023 12:18:31 +0200 |
wenzelm |
proper sync_database for receive timeout;
|
file |
diff |
annotate
|
| Tue, 22 Aug 2023 11:54:06 +0200 |
wenzelm |
clarified source structure;
|
file |
diff |
annotate
|
| Mon, 21 Aug 2023 15:04:22 +0200 |
wenzelm |
clarified signature: proper treatment of implicit state (amending d0c9d277620e);
|
file |
diff |
annotate
|
| Mon, 21 Aug 2023 12:34:53 +0200 |
wenzelm |
clarified signature: more robust treatment of implicit state;
|
file |
diff |
annotate
|
| Mon, 21 Aug 2023 11:56:07 +0200 |
wenzelm |
proper sync_database for Database_Progress consumer;
|
file |
diff |
annotate
|
| Mon, 21 Aug 2023 11:43:29 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Mon, 21 Aug 2023 11:42:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 20 Aug 2023 22:24:24 +0200 |
wenzelm |
limit size and complexity of bulk transactions;
|
file |
diff |
annotate
|
| Sat, 19 Aug 2023 22:57:06 +0200 |
wenzelm |
clarified signature: filter batch;
|
file |
diff |
annotate
|
| Sat, 19 Aug 2023 14:45:57 +0200 |
wenzelm |
more scalable write_messages via db.execute_batch_statement;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2023 20:13:49 +0200 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2023 20:06:24 +0200 |
wenzelm |
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2023 19:01:40 +0200 |
wenzelm |
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2023 14:46:24 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 16 Aug 2023 14:42:43 +0200 |
wenzelm |
build_worker is stopped independently from master build_process;
|
file |
diff |
annotate
|
| Thu, 10 Aug 2023 16:57:01 +0200 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Thu, 10 Aug 2023 16:49:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 10 Aug 2023 16:40:07 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 22 Jul 2023 12:10:03 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 18 Jul 2023 12:19:12 +0200 |
wenzelm |
clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
|
file |
diff |
annotate
|
| Mon, 17 Jul 2023 20:31:45 +0200 |
wenzelm |
clarified errors;
|
file |
diff |
annotate
|
| Sun, 16 Jul 2023 11:29:23 +0200 |
wenzelm |
more informative trace;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2023 13:13:10 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 07 Jul 2023 14:17:53 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2023 20:09:12 +0200 |
wenzelm |
more robust "stop": further "stamp" ticks may happen afterwards;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2023 18:56:52 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2023 15:25:12 +0200 |
wenzelm |
more SQL data;
|
file |
diff |
annotate
|
| Wed, 21 Jun 2023 14:27:51 +0200 |
wenzelm |
clarified signature: more explicit class SQL.Data;
|
file |
diff |
annotate
|
| Fri, 16 Jun 2023 14:20:18 +0200 |
wenzelm |
proper support for SQLite: avoid conflicts on transaction_lock;
|
file |
diff |
annotate
|
| Wed, 14 Jun 2023 16:27:44 +0200 |
wenzelm |
prefer Database_Progress, which is more robust (amending afb1a19307c4);
|
file |
diff |
annotate
|
| Wed, 14 Jun 2023 15:37:30 +0200 |
wenzelm |
support for Database_Progress;
|
file |
diff |
annotate
|
| Sun, 05 Mar 2023 18:38:52 +0100 |
wenzelm |
more robust: disallow override;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 22:29:21 +0100 |
wenzelm |
clarified treatment of "verbose" messages, e.g. Progress.theory();
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 21:25:12 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 17:36:29 +0100 |
wenzelm |
more robust signature: avoid totally adhoc overriding (see also Build_Process.progress vs. build_progress);
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 16:15:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 12:59:22 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 12:43:35 +0100 |
wenzelm |
clarified signature: require just one "override def echo(message: Progress.Message): Unit";
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 12:05:51 +0100 |
wenzelm |
clarified signature: more uniform Progress.verbose, avoid adhoc "override def theory()";
|
file |
diff |
annotate
|
| Sat, 04 Mar 2023 11:45:14 +0100 |
wenzelm |
proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo;
|
file |
diff |
annotate
|
| Wed, 01 Feb 2023 21:23:54 +0100 |
wenzelm |
more general program start message;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 19:43:45 +0100 |
wenzelm |
proper program name, e.g. for session "Intro";
|
file |
diff |
annotate
|
| Mon, 16 Jan 2023 22:41:00 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 16 Jan 2023 20:08:15 +0100 |
wenzelm |
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
|
file |
diff |
annotate
|
| Wed, 07 Dec 2022 21:02:43 +0100 |
wenzelm |
clarified signature: just one level of arguments to avoid type-inference problems;
|
file |
diff |
annotate
|
| Wed, 07 Dec 2022 15:43:47 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2021 11:35:07 +0200 |
wenzelm |
clarified signature: prefer Java interfaces;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 12:52:00 +0100 |
wenzelm |
clarified document_output vs. progress;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2020 21:59:17 +0100 |
wenzelm |
proper message;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2020 21:23:12 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 16:27:31 +0100 |
wenzelm |
more interrupts, notably for running latex;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 21:00:14 +0100 |
wenzelm |
build documents in Isabelle/Scala, based on generated tex files as session exports;
|
file |
diff |
annotate
|
| Tue, 07 Apr 2020 21:49:36 +0200 |
wenzelm |
clarified signature: more uniform treatment of stopped/interrupted state;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2019 16:02:29 +0100 |
wenzelm |
clarified Console_Progress.echo: include empty lines as in other Progress instances, especially relevant for Progress.bash (e.g. "isabelle phabricator ./bin/config help");
|
file |
diff |
annotate
|
| Mon, 18 Feb 2019 15:57:06 +0100 |
wenzelm |
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
|
file |
diff |
annotate
|
| Sun, 17 Feb 2019 22:15:02 +0100 |
wenzelm |
clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
|
file |
diff |
annotate
|
| Thu, 13 Sep 2018 11:41:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 09 Sep 2018 11:53:53 +0200 |
wenzelm |
clarified theory progress;
|
file |
diff |
annotate
|
| Sat, 08 Sep 2018 21:48:26 +0200 |
wenzelm |
more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;
|
file |
diff |
annotate
|
| Tue, 04 Sep 2018 14:40:31 +0200 |
wenzelm |
clarified Nodes_Status;
|
file |
diff |
annotate
|
| Mon, 03 Sep 2018 20:04:51 +0200 |
wenzelm |
more detailed progress;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 23:25:53 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 18 Aug 2018 22:09:09 +0200 |
wenzelm |
optional notification of nodes_status (via progress);
|
file |
diff |
annotate
|
| Sat, 09 Jun 2018 21:52:16 +0200 |
wenzelm |
clarified signature: more uniform theory_message (see also d7920eb7de54);
|
file |
diff |
annotate
|
| Wed, 30 May 2018 14:34:43 +0200 |
wenzelm |
report theory progress via PIDE node status;
|
file |
diff |
annotate
|
| Mon, 28 May 2018 13:35:43 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2018 16:38:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2017 20:29:00 +0100 |
wenzelm |
avoid println with its extra CR on Windows;
|
file |
diff |
annotate
|
| Fri, 26 May 2017 11:09:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 25 May 2017 17:32:35 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Tue, 23 May 2017 11:47:35 +0200 |
wenzelm |
clarified build.out progress;
|
file |
diff |
annotate
|
| Sun, 21 May 2017 20:11:12 +0200 |
wenzelm |
more Progress variations;
|
file |
diff |
annotate
|
| Sun, 14 May 2017 17:05:06 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 14 May 2017 17:00:57 +0200 |
wenzelm |
clarified interface;
|
file |
diff |
annotate
|
| Mon, 16 Jan 2017 21:53:44 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 13 Oct 2016 23:09:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 08 Oct 2016 22:36:22 +0200 |
wenzelm |
build_history log files with formal meta info;
|
file |
diff |
annotate
|
| Wed, 05 Oct 2016 11:43:00 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2015 13:54:04 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|