incorporate timing into Node_Status, while the default threshold leads to empty command_timings;

--- a/src/Pure/PIDE/document_status.scala	Wed Sep 17 17:29:29 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Wed Sep 17 20:13:18 2025 +0200
@@ -180,7 +180,8 @@
     def make(
       state: Document.State,
       version: Document.Version,
-      name: Document.Node.Name
+      name: Document.Node.Name,
+      threshold: Time = Time.max
     ): Node_Status = {
       var unprocessed = 0
       var running = 0
@@ -189,7 +190,10 @@
       var finished = 0
       var canceled = false
       var terminated = true
+      var total_time = Time.zero
+      var command_timings = Map.empty[Command, Time]
       var theory_status = Document_Status.Theory_Status.NONE
+
       for (command <- version.nodes(name).commands.iterator) {
         val status = state.command_status(version, command)
 
@@ -202,6 +206,10 @@
         if (status.is_canceled) canceled = true
         if (!status.is_terminated) terminated = false
 
+        val t = state.command_timing(version, command).elapsed
+        total_time += t
+        if (t.is_notable(threshold)) command_timings += (command -> t)
+
         theory_status = Theory_Status.merge(theory_status, status.theory_status)
       }
 
@@ -214,6 +222,9 @@
         finished = finished,
         canceled = canceled,
         terminated = terminated,
+        total_time = total_time,
+        threshold = threshold,
+        command_timings = command_timings,
         theory_status = theory_status)
     }
   }
@@ -227,7 +238,10 @@
     finished: Int = 0,
     canceled: Boolean = false,
     terminated: Boolean = false,
-    theory_status: Theory_Status.Value = Theory_Status.NONE
+    total_time: Time = Time.zero,
+    threshold: Time = Time.zero,
+    command_timings: Map[Command, Time] = Map.empty,
+    theory_status: Theory_Status.Value = Theory_Status.NONE,
   ) extends Theory_Status {
     def is_empty: Boolean = this == Node_Status.empty
 
@@ -249,34 +263,6 @@
   }
 
 
-  /* overall timing */
-
-  object Overall_Timing {
-    val empty: Overall_Timing = Overall_Timing()
-
-    def make(
-      state: Document.State,
-      version: Document.Version,
-      name: Document.Node.Name,
-      threshold: Time = Time.zero
-    ): Overall_Timing = {
-      var total = Time.zero
-      var command_timings = Map.empty[Command, Time]
-      for (command <- version.nodes(name).commands.iterator) {
-        val timing = state.command_timing(version, command)
-        total += timing.elapsed
-        if (timing.is_notable(threshold)) command_timings += (command -> timing.elapsed)
-      }
-      Overall_Timing(total = total, threshold = threshold, command_timings = command_timings)
-    }
-  }
-
-  sealed case class Overall_Timing(
-    total: Time = Time.zero,
-    threshold: Time = Time.zero,
-    command_timings: Map[Command, Time] = Map.empty)
-
-
   /* nodes status */
 
   enum Overall_Status { case ok, failed, pending }
@@ -293,6 +279,8 @@
     def apply(name: Document.Node.Name): Node_Status = rep.getOrElse(name, Node_Status.empty)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
+    def iterator: Iterator[(Document.Node.Name, Node_Status)] = rep.iterator
+
     def present(
       domain: Option[List[Document.Node.Name]] = None
     ): List[(Document.Node.Name, Node_Status)] = {
@@ -317,6 +305,7 @@
       resources: Resources,
       state: Document.State,
       version: Document.Version,
+      threshold: Time = Time.max,
       domain: Option[Set[Document.Node.Name]] = None,
       trim: Boolean = false
     ): (Boolean, Nodes_Status) = {
@@ -325,7 +314,7 @@
         for {
           name <- domain.getOrElse(nodes1.domain).iterator
           if !Resources.hidden_node(name) && !resources.loaded_theory(name)
-          st = Document_Status.Node_Status.make(state, version, name)
+          st = Document_Status.Node_Status.make(state, version, name, threshold = threshold)
           if apply(name) != st
         } yield (name -> st)
       val rep1 = rep ++ update_iterator

--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Sep 17 17:29:29 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Wed Sep 17 20:13:18 2025 +0200
@@ -131,7 +131,7 @@
 
   /* component state -- owned by GUI thread */
 
-  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing]
+  private var nodes_status = Document_Status.Nodes_Status.empty
 
   private def make_entries(): List[Entry] = {
     GUI_Thread.require {}
@@ -141,13 +141,13 @@
         case None => Document.Node.Name.empty
         case Some(doc_view) => doc_view.model.node_name
       }
-    val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty)
 
     val theories =
-      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
-        yield Theory_Entry(node_name, node_timing.total.seconds)).sorted(Entry.Ordering)
+      List.from(
+        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) <- timing.command_timings.toList)
+      (for ((command, command_timing) <- nodes_status(name).command_timings.toList)
         yield Command_Entry(command, command_timing.seconds)).sorted(Entry.Ordering)
 
     theories.flatMap(entry =>
@@ -160,22 +160,15 @@
 
     val snapshot = PIDE.session.snapshot()
 
-    val nodes_timing1 =
-      (restriction match {
-        case Some(names) => names.iterator
-        case None => snapshot.version.nodes.names_iterator
-      }).foldLeft(nodes_timing) {
-          case (timing1, name) =>
-            if (PIDE.resources.loaded_theory(name)) timing1
-            else {
-              val node_timing =
-                Document_Status.Overall_Timing.make(
-                  snapshot.state, snapshot.version, name,
-                  threshold = Time.seconds(timing_threshold))
-              timing1 + (name -> node_timing)
-            }
-        }
-    nodes_timing = nodes_timing1
+    val domain =
+      restriction.getOrElse(
+        snapshot.version.nodes.names_iterator
+          .filterNot(PIDE.resources.loaded_theory).toSet)
+
+    nodes_status =
+      nodes_status.update(PIDE.resources, snapshot.state, snapshot.version,
+        threshold = Time.seconds(timing_threshold),
+        domain = Some(domain))._2
 
     val entries = make_entries()
     if (timing_view.listData.toList != entries) timing_view.listData = entries