src/Pure/PIDE/document_status.scala

--- 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 */