src/Pure/PIDE/document_status.scala

 
     def make(
       state: Document.State,
       version: Document.Version,
       commands: Iterable[Command],
-      threshold: Double): Overall_Timing =
+      threshold: Double = 0.0): Overall_Timing =
     {
       var total = 0.0
       var command_timings = Map.empty[Command, Double]
       for {
         command <- commands.iterator

           (0.0 /: st.status)({
             case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
             case (timing, _) => timing
           })
         total += command_timing
-        if (command_timing >= threshold) command_timings += (command -> command_timing)
+        if (command_timing > 0.0 && command_timing >= threshold) {
+          command_timings += (command -> command_timing)
+        }
       }
       Overall_Timing(total, command_timings)
     }
   }
 
   sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
+  {
+    def command_timing(command: Command): Double =
+      command_timings.getOrElse(command, 0.0)
+  }
 
 
   /* nodes status */
 
   object Overall_Node_Status extends Enumeration