# HG changeset patch
# User wenzelm
# Date 1551789093 -3600
# Node ID d594997cdcf47a20b347c4496923df1f3887c794
# Parent  9532d5b2e932b3b9f0cc23f42701e31e409b98f0
clarified signature;

diff -r 9532d5b2e932 -r d594997cdcf4 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Tue Mar 05 13:11:01 2019 +0100
+++ b/src/Pure/PIDE/document_status.scala	Tue Mar 05 13:31:33 2019 +0100
@@ -189,7 +189,7 @@
       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]
@@ -203,13 +203,19 @@
             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 */
diff -r 9532d5b2e932 -r d594997cdcf4 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 13:11:01 2019 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Mar 05 13:31:33 2019 +0100
@@ -192,7 +192,7 @@
           else {
             val node_timing =
               Document_Status.Overall_Timing.make(
-                snapshot.state, snapshot.version, node.commands, timing_threshold)
+                snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
             timing1 + (name -> node_timing)
           }
       })