# HG changeset patch
# User wenzelm
# Date 1758620080 -7200
# Node ID f143ff394324bd8719761943f05ef610b45795ff
# Parent  7409cb179fba5ed8537cf69bcd9f26b36a597bde
clarified signature;

diff -r 7409cb179fba -r f143ff394324 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Mon Sep 22 22:02:59 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 23 11:34:40 2025 +0200
@@ -238,7 +238,7 @@
       var terminated = true
       var total_time = Time.zero
       var max_time = Time.zero
-      var command_timings = Map.empty[Command, Time]
+      var command_timings = Map.empty[Command, Command_Timings]
       var theory_status = Document_Status.Theory_Status.NONE
 
       for (command <- version.nodes(name).commands.iterator) {
@@ -256,7 +256,7 @@
         val t = status.timings.sum.elapsed
         total_time += t
         if (t > max_time) max_time = t
-        if (t.is_notable(threshold)) command_timings += (command -> t)
+        if (t.is_notable(threshold)) command_timings += (command -> status.timings)
 
         theory_status = Theory_Status.merge(theory_status, status.theory_status)
       }
@@ -290,7 +290,7 @@
     total_time: Time = Time.zero,
     max_time: Time = Time.zero,
     threshold: Time = Time.zero,
-    command_timings: Map[Command, Time] = Map.empty,
+    command_timings: Map[Command, Command_Timings] = Map.empty,
     theory_status: Theory_Status.Value = Theory_Status.NONE,
   ) extends Theory_Status {
     def is_empty: Boolean = this == Node_Status.empty
diff -r 7409cb179fba -r f143ff394324 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Sep 22 22:02:59 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Sep 23 11:34:40 2025 +0200
@@ -147,8 +147,8 @@
         for ((a, st) <- nodes_status.iterator if st.command_timings.nonEmpty)
           yield Theory_Entry(a, st.total_time.seconds)).sorted(Entry.Ordering)
     val commands =
-      (for ((command, command_timing) <- nodes_status(name).command_timings.toList)
-        yield Command_Entry(command, command_timing.seconds)).sorted(Entry.Ordering)
+      (for ((command, timings) <- nodes_status(name).command_timings.toList)
+        yield Command_Entry(command, timings.sum.elapsed.seconds)).sorted(Entry.Ordering)
 
     theories.flatMap(entry =>
       if (entry.name == name) entry.make_current :: commands