src/Pure/PIDE/document_status.scala

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 15:42:02 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 16 15:56:28 2025 +0200
@@ -227,7 +227,7 @@
       state: Document.State,
       version: Document.Version,
       commands: Iterable[Command],
-      threshold: Double = 0.0
+      threshold: Time = Time.zero
     ): Overall_Timing = {
       var total = 0.0
       var command_timings = Map.empty[Command, Double]
@@ -235,7 +235,7 @@
         val timing = state.command_timing(version, command)
         val elapsed = timing.elapsed.seconds
         total += elapsed
-        if (timing.is_relevant && elapsed >= threshold) command_timings += (command -> elapsed)
+        if (timing.is_notable(threshold)) command_timings += (command -> elapsed)
       }
       Overall_Timing(total = total, command_timings = command_timings)
     }