src/Pure/PIDE/rendering.scala

--- a/src/Pure/PIDE/rendering.scala	Tue Sep 16 14:19:34 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Sep 16 15:21:35 2025 +0200
@@ -268,7 +268,7 @@
       Markup.COMMAND_SPAN)
 
   val tooltip_elements: Markup.Elements =
-    Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION, Markup.TIMING,
+    Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION,
       Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
       Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.COMMAND_SPAN,
       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
@@ -621,11 +621,9 @@
 
   private sealed case class Tooltip_Info(
     range: Text.Range,
-    timing: Timing = Timing.zero,
     messages: List[(Long, XML.Elem)] = Nil,
     rev_infos: List[(Boolean, Int, XML.Elem)] = Nil
   ) {
-    def add_timing(t: Timing): Tooltip_Info = copy(timing = timing + t)
     def add_message(r0: Text.Range, serial: Long, msg: XML.Elem): Tooltip_Info = {
       val r = snapshot.convert(r0)
       if (range == r) copy(messages = (serial -> msg) :: messages)
@@ -643,19 +641,8 @@
     def add_info_text(r0: Text.Range, text: String, ord: Int = 0): Tooltip_Info =
       add_info(r0, Pretty.string(text), ord = ord)
 
-    def timing_info(elem: XML.Elem): Option[XML.Elem] =
-      if (elem.markup.name == Markup.TIMING) {
-        if (timing.is_relevant && timing.elapsed.seconds >= timing_threshold) {
-          Some(Pretty.string(timing.message))
-        }
-        else None
-      }
-      else Some(elem)
     def infos(important: Boolean = true): List[XML.Elem] =
-      for {
-        (is_important, _, elem) <- rev_infos.reverse.sortBy(_._2) if is_important == important
-        elem1 <- timing_info(elem)
-      } yield elem1
+      for ((imp, _, elem) <- rev_infos.reverse.sortBy(_._2) if imp == important) yield elem
   }
 
   def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
@@ -666,8 +653,6 @@
     val results =
       snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states =>
         {
-          case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info.add_timing(t))
-
           case (info, Text.Info(r0, msg @ XML.Elem(Markup.Bad(i), body)))
           if body.nonEmpty => Some(info.add_message(r0, i, msg))
 
@@ -680,7 +665,16 @@
           if kind != "" && kind != Markup.ML_DEF =>
             val txt = Rendering.gui_name(name, kind = kind)
             val info1 = info.add_info_text(r0, txt, ord = 2)
-            Some(if (kind == Markup.COMMAND) info1.add_info(r0, XML.elem(Markup.TIMING)) else info1)
+            val info2 =
+              if (kind == Markup.COMMAND) {
+                val timing = Timing.merge(command_states.iterator.map(_.timing))
+                if (timing.is_relevant && timing.elapsed.seconds >= timing_threshold) {
+                  info1.add_info(r0, Pretty.string(timing.message))
+                }
+                else info1
+              }
+              else info1
+            Some(info2)
 
           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
             val file = perhaps_append_file(snapshot.node_name, name)