| Fri, 17 Oct 2025 15:19:01 +0200 |
wenzelm |
clarified status_theories: show only running or updated theories;
|
file |
diff |
annotate
|
| Fri, 17 Oct 2025 15:13:45 +0200 |
wenzelm |
clarified command_timing protocol: support for still running commands, with timing approximated in Isabelle/Scala;
|
file |
diff |
annotate
|
| Fri, 17 Oct 2025 11:03:16 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2025 14:31:35 +0200 |
wenzelm |
clarified markup: re-use protocol function name;
|
file |
diff |
annotate
|
| Wed, 15 Oct 2025 22:57:19 +0200 |
wenzelm |
clarified command_timing: expose elapsed time only, other fields were never used;
|
file |
diff |
annotate
|
| Sun, 12 Oct 2025 15:11:29 +0200 |
wenzelm |
more detailed Console_Progress via Progress.Status;
|
file |
diff |
annotate
|
| Mon, 06 Oct 2025 18:01:21 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Mon, 06 Oct 2025 17:43:00 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 24 Sep 2025 22:47:04 +0200 |
wenzelm |
build_progress with percentage;
|
file |
diff |
annotate
|
| Wed, 24 Sep 2025 22:18:52 +0200 |
wenzelm |
clarified signature: prefer static percentage;
|
file |
diff |
annotate
|
| Wed, 24 Sep 2025 16:22:49 +0200 |
wenzelm |
more accurate theory timing, based on sum of command timings;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2025 11:39:47 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2025 11:34:40 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2025 17:20:06 +0200 |
wenzelm |
avoid shortcuts based on potentially expensive equality test;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2025 14:01:37 +0200 |
wenzelm |
more detailed Command_Timings: count actual commands from theory body individually;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2025 19:47:26 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2025 14:28:42 +0200 |
wenzelm |
clarified signature: prefer explicit operations;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2025 14:22:14 +0200 |
wenzelm |
clarified signature: explicit domain for Nodes_Status operations;
|
file |
diff |
annotate
|
| Sat, 20 Sep 2025 16:34:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2025 20:36:28 +0200 |
wenzelm |
more informative Node_Status;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2025 20:13:18 +0200 |
wenzelm |
incorporate timing into Node_Status, while the default threshold leads to empty command_timings;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2025 17:29:29 +0200 |
wenzelm |
more robust: total "apply", with subtle change of semantics;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2025 13:00:51 +0200 |
wenzelm |
more scalable timing, as part of incremental document_status;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2025 11:41:27 +0200 |
wenzelm |
tuned signature: more explicit operations;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2025 11:30:59 +0200 |
wenzelm |
tuned signature: more explicit operations;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 21:04:39 +0200 |
wenzelm |
more scalable Command.State.document_status: prefer incremental update;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 16:40:07 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 16:37:43 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 16:30:30 +0200 |
wenzelm |
clarified signature: more explicit data;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 16:27:14 +0200 |
wenzelm |
clarified signature: more uniform Node_Status.make vs. Overall_Timing.make;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 15:56:28 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 15:42:02 +0200 |
wenzelm |
more uniform treatment of timing threshold;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 13:52:24 +0200 |
wenzelm |
clarified signature: more thorough treatment of all command_states;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 13:46:43 +0200 |
wenzelm |
clarified signature and persistent data;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 12:32:13 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 12:24:12 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 12:06:07 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 11:58:46 +0200 |
wenzelm |
more uniform Command_Status.theory_status vs. Node_Status.theory_status: cover all command_states, without special cases;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 11:23:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2025 10:39:53 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2025 23:25:20 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2025 23:07:57 +0200 |
wenzelm |
clarified Theory_Status.FINALIZED: it belongs to this linear row, too;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2025 22:36:04 +0200 |
wenzelm |
clarified signature: more explicit type Theory_Status;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2025 18:09:55 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2025 17:42:09 +0200 |
wenzelm |
clarified signature, following e.g. Command.Markups;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2025 17:28:22 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2025 16:57:56 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 28 Jul 2025 16:10:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 16:42:08 +0200 |
wenzelm |
clarified signature: prefer enum types;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 16:34:13 +0100 |
wenzelm |
clarified state document nodes for Theories_Status / Document_Dockable;
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 15:29:24 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 11 Nov 2021 22:06:18 +0100 |
wenzelm |
clarified signature: prefer static operations;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 23:17:47 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 11:32:38 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Wed, 04 Sep 2019 22:00:38 +0200 |
wenzelm |
load theories in stages, to reduce ML heap requirements;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2019 13:31:33 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2019 13:11:01 +0100 |
wenzelm |
clarified signature: more general types;
|
file |
diff |
annotate
|