diff -r a39fde2f020a -r 9cc5d77d505c src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Sep 21 23:48:59 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Sep 22 14:01:37 2025 +0200
@@ -667,9 +667,9 @@
             val info1 = info.add_info_text(r0, txt, ord = 2)
             val info2 =
               if (kind == Markup.COMMAND) {
-                val timing = Timing.merge(command_states.iterator.map(_.timing))
-                if (timing.is_notable(timing_threshold)) {
-                  info1.add_info(r0, Pretty.string(timing.message))
+                val t = Document_Status.Command_Timings.merge(command_states.map(_.timings)).sum
+                if (t.is_notable(timing_threshold)) {
+                  info1.add_info(r0, Pretty.string(t.message))
                 }
                 else info1
               }