diff -r 9cc5d77d505c -r 1d189ef55adf src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Sep 22 14:01:37 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Sep 22 15:55:47 2025 +0200
@@ -661,13 +661,14 @@
             for ((i, msg) <- Command.State.get_result_proper(command_states, props))
             yield info.add_message(r0, i, msg)
 
-          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
+          case (info, Text.Info(r0, XML.Elem(markup@Markup.Entity(kind, name), _)))
           if kind != "" && kind != Markup.ML_DEF =>
             val txt = Rendering.gui_name(name, kind = kind)
             val info1 = info.add_info_text(r0, txt, ord = 2)
             val info2 =
               if (kind == Markup.COMMAND) {
-                val t = Document_Status.Command_Timings.merge(command_states.map(_.timings)).sum
+                val timings = Document_Status.Command_Timings.merge(command_states.map(_.timings))
+                val t = timings(Markup.Command_Offset.get(markup.properties))
                 if (t.is_notable(timing_threshold)) {
                   info1.add_info(r0, Pretty.string(t.message))
                 }