src/Pure/PIDE/document_status.scala

       var warned1 = warned
       var failed1 = failed
       var canceled = false
       var forks = 0
       var runs = 0
+      var timing = Timing.zero
       for (markup <- markups) {
         markup.name match {
           case Markup.INITIALIZED =>
             theory_status = Theory_Status.merge(theory_status, Theory_Status.INITIALIZED)
           case Markup.FINALIZED =>

           case Markup.WARNING | Markup.LEGACY => warned1 = true
           case Markup.FAILED | Markup.ERROR => failed1 = true
           case Markup.CANCELED => canceled = true
           case _ =>
         }
+        markup match {
+          case Markup.Timing(t) => timing += t
+          case _ =>
+        }
       }
       new Command_Status(
         theory_status = theory_status,
         touched = touched,
         accepted = accepted,
         warned = warned1,
         failed = failed1,
         canceled = canceled,
         forks = forks,
-        runs = runs)
+        runs = runs,
+        timing = timing)
     }
 
     val empty: Command_Status = make()
 
     def merge(args: IterableOnce[Command_Status]): Command_Status =

     private val accepted: Boolean,
     private val warned: Boolean,
     private val failed: Boolean,
     private val canceled: Boolean,
     val forks: Int,
-    val runs: Int
+    val runs: Int,
+    val timing: Timing
   ) extends Theory_Status {
     override def toString: String =
       if (is_empty) "Command_Status.empty"
       else if (failed) "Command_Status(failed)"
       else if (warned) "Command_Status(warned)"
       else "Command_Status(...)"
 
     def is_empty: Boolean =
       !Theory_Status.initialized(theory_status) &&
       !touched && !accepted && !warned && !failed && !canceled &&
-      forks == 0 && runs == 0
+      forks == 0 && runs == 0 && timing.is_zero
 
     def + (that: Command_Status): Command_Status =
       if (is_empty) that
       else if (that.is_empty) this
       else {

           accepted = accepted || that.accepted,
           warned = warned || that.warned,
           failed = failed || that.failed,
           canceled = canceled || that.canceled,
           forks = forks + that.forks,
-          runs = runs + that.runs)
+          runs = runs + that.runs,
+          timing = timing + that.timing)
       }
 
     def update(
       markups: List[Markup] = Nil,
       warned: Boolean = false,

             accepted = accepted,
             warned = warned1,
             failed = failed1,
             canceled = canceled,
             forks = forks,
-            runs = runs)
+            runs = runs,
+            timing = timing)
         }
       }
       else this + Command_Status.make(markups = markups, warned = warned, failed = failed)
     }