clarified signature: more general types;

--- a/src/Pure/PIDE/document_status.scala	Tue Mar 05 11:52:20 2019 +0100
+++ b/src/Pure/PIDE/document_status.scala	Tue Mar 05 13:11:01 2019 +0100
@@ -179,22 +179,22 @@
   }
 
 
-  /* node timing */
+  /* overall timing */
 
-  object Node_Timing
+  object Overall_Timing
   {
-    val empty: Node_Timing = Node_Timing(0.0, Map.empty)
+    val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
 
     def make(
       state: Document.State,
       version: Document.Version,
-      node: Document.Node,
-      threshold: Double): Node_Timing =
+      commands: Iterable[Command],
+      threshold: Double): Overall_Timing =
     {
       var total = 0.0
-      var commands = Map.empty[Command, Double]
+      var command_timings = Map.empty[Command, Double]
       for {
-        command <- node.commands.iterator
+        command <- commands.iterator
         st <- state.command_states(version, command)
       } {
         val command_timing =
@@ -203,13 +203,13 @@
             case (timing, _) => timing
           })
         total += command_timing
-        if (command_timing >= threshold) commands += (command -> command_timing)
+        if (command_timing >= threshold) command_timings += (command -> command_timing)
       }
-      Node_Timing(total, commands)
+      Overall_Timing(total, command_timings)
     }
   }
 
-  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
+  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
 
 
   /* nodes status */

--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 11:52:20 2019 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 13:11:01 2019 +0100
@@ -150,7 +150,7 @@
 
   /* component state -- owned by GUI thread */
 
-  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Node_Timing]
+  private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing]
 
   private def make_entries(): List[Entry] =
   {
@@ -161,13 +161,13 @@
         case None => Document.Node.Name.empty
         case Some(doc_view) => doc_view.model.node_name
       }
-    val timing = nodes_timing.getOrElse(name, Document_Status.Node_Timing.empty)
+    val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty)
 
     val theories =
-      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.commands.nonEmpty)
+      (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
         yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
     val commands =
-      (for ((command, command_timing) <- timing.commands.toList)
+      (for ((command, command_timing) <- timing.command_timings.toList)
         yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
 
     theories.flatMap(entry =>
@@ -191,8 +191,8 @@
           if (PIDE.resources.session_base.loaded_theory(name)) timing1
           else {
             val node_timing =
-              Document_Status.Node_Timing.make(
-                snapshot.state, snapshot.version, node, timing_threshold)
+              Document_Status.Overall_Timing.make(
+                snapshot.state, snapshot.version, node.commands, timing_threshold)
             timing1 + (name -> node_timing)
           }
       })