src/Pure/PIDE/document_status.scala
Fri, 17 Oct 2025 15:19:01 +0200 wenzelm clarified status_theories: show only running or updated theories;
Fri, 17 Oct 2025 15:13:45 +0200 wenzelm clarified command_timing protocol: support for still running commands, with timing approximated in Isabelle/Scala;
Fri, 17 Oct 2025 11:03:16 +0200 wenzelm unused;
Thu, 16 Oct 2025 14:31:35 +0200 wenzelm clarified markup: re-use protocol function name;
Wed, 15 Oct 2025 22:57:19 +0200 wenzelm clarified command_timing: expose elapsed time only, other fields were never used;
Sun, 12 Oct 2025 15:11:29 +0200 wenzelm more detailed Console_Progress via Progress.Status;
Mon, 06 Oct 2025 18:01:21 +0200 wenzelm minor performance tuning;
Mon, 06 Oct 2025 17:43:00 +0200 wenzelm tuned signature;
Wed, 24 Sep 2025 22:47:04 +0200 wenzelm build_progress with percentage;
Wed, 24 Sep 2025 22:18:52 +0200 wenzelm clarified signature: prefer static percentage;
Wed, 24 Sep 2025 16:22:49 +0200 wenzelm more accurate theory timing, based on sum of command timings;
Tue, 23 Sep 2025 11:39:47 +0200 wenzelm tuned signature;
Tue, 23 Sep 2025 11:34:40 +0200 wenzelm clarified signature;
Mon, 22 Sep 2025 17:20:06 +0200 wenzelm avoid shortcuts based on potentially expensive equality test;
Mon, 22 Sep 2025 14:01:37 +0200 wenzelm more detailed Command_Timings: count actual commands from theory body individually;
Sun, 21 Sep 2025 19:47:26 +0200 wenzelm clarified signature;
Sun, 21 Sep 2025 14:28:42 +0200 wenzelm clarified signature: prefer explicit operations;
Sun, 21 Sep 2025 14:22:14 +0200 wenzelm clarified signature: explicit domain for Nodes_Status operations;
Sat, 20 Sep 2025 16:34:32 +0200 wenzelm tuned;
Wed, 17 Sep 2025 20:36:28 +0200 wenzelm more informative Node_Status;
Wed, 17 Sep 2025 20:13:18 +0200 wenzelm incorporate timing into Node_Status, while the default threshold leads to empty command_timings;
Wed, 17 Sep 2025 17:29:29 +0200 wenzelm more robust: total "apply", with subtle change of semantics;
Wed, 17 Sep 2025 13:00:51 +0200 wenzelm more scalable timing, as part of incremental document_status;
Wed, 17 Sep 2025 11:41:27 +0200 wenzelm tuned signature: more explicit operations;
Wed, 17 Sep 2025 11:30:59 +0200 wenzelm tuned signature: more explicit operations;
Tue, 16 Sep 2025 21:04:39 +0200 wenzelm more scalable Command.State.document_status: prefer incremental update;
Tue, 16 Sep 2025 16:40:07 +0200 wenzelm unused;
Tue, 16 Sep 2025 16:37:43 +0200 wenzelm clarified signature: more explicit types;
Tue, 16 Sep 2025 16:30:30 +0200 wenzelm clarified signature: more explicit data;
Tue, 16 Sep 2025 16:27:14 +0200 wenzelm clarified signature: more uniform Node_Status.make vs. Overall_Timing.make;
less more (0) -50 -30 tip