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