src/Pure/PIDE/document_status.scala

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 15:21:35 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 16 15:42:02 2025 +0200
@@ -232,11 +232,10 @@
       var total = 0.0
       var command_timings = Map.empty[Command, Double]
       for (command <- commands.iterator) {
-        val command_timing = state.command_timing(version, command).elapsed.seconds
-        total += command_timing
-        if (command_timing > 0.0 && command_timing >= threshold) {
-          command_timings += (command -> command_timing)
-        }
+        val timing = state.command_timing(version, command)
+        val elapsed = timing.elapsed.seconds
+        total += elapsed
+        if (timing.is_relevant && elapsed >= threshold) command_timings += (command -> elapsed)
       }
       Overall_Timing(total = total, command_timings = command_timings)
     }