src/Pure/PIDE/rendering.scala

     Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name, Markup.ENTITY,
       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) ++
       Markup.Elements(tooltip_description.keySet)
 

 
   def timing_threshold: Double = options.real("editor_timing_threshold")
 
   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)
       else copy(range = r, messages = List(serial -> msg))
     }

       else copy (range = r, rev_infos = List(entry))
     }
     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 =
     if (Path.is_valid(name)) session.resources.append_path(node_name.master_dir, Path.explode(name))
     else name
 
   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Elem]]] = {
     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))
 
           case (info, Text.Info(r0, XML.Elem(Markup(name, props), _)))
           if Rendering.tooltip_message_elements(name) =>

 
           case (info, Text.Info(r0, XML.Elem(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)
-            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)
             val info1 =
               if (name == file) info