src/Pure/PIDE/rendering.scala

   }
 
 
   /* tooltips */
 
-  def timing_threshold: Double = 0.0
+  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,

     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.elapsed.seconds >= timing_threshold) {
+        if (timing.is_relevant && timing.elapsed.seconds >= timing_threshold) {
           Some(Pretty.string(timing.message))
         }
         else None
       }
       else Some(elem)