src/Pure/PIDE/document_status.scala

 
 object Document_Status {
   /* command status */
 
   object Command_Status {
+    object Theory_Status extends Enumeration {
+      val NONE, INITIALIZED, CONSOLIDATING, CONSOLIDATED = Value
+
+      def initialized(t: Value): Boolean = t >= INITIALIZED
+      def consolidating(t: Value): Boolean = t >= CONSOLIDATING
+      def consolidated(t: Value): Boolean = t >= CONSOLIDATED
+
+      def merge(t1: Value, t2: Value): Value = if (t1 >= t2) t1 else t2
+    }
+
     val proper_elements: Markup.Elements =
       Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
         Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
 
     val liberal_elements: Markup.Elements =

     def make(
       markups: Iterable[Markup],
       warned: Boolean = false,
       failed: Boolean = false
     ): Command_Status = {
+      var theory_status = Theory_Status.NONE
       var touched = false
       var accepted = false
       var warned1 = warned
       var failed1 = failed
       var canceled = false
       var finalized = false
       var forks = 0
       var runs = 0
       for (markup <- markups) {
         markup.name match {
+          case Markup.INITIALIZED =>
+            theory_status = Theory_Status.merge(theory_status, Theory_Status.INITIALIZED)
+          case Markup.CONSOLIDATING =>
+            theory_status = Theory_Status.merge(theory_status, Theory_Status.CONSOLIDATING)
+          case Markup.CONSOLIDATED =>
+            theory_status = Theory_Status.merge(theory_status, Theory_Status.CONSOLIDATED)
           case Markup.ACCEPTED => accepted = true
           case Markup.FORKED => touched = true; forks += 1
           case Markup.JOINED => forks -= 1
           case Markup.RUNNING => touched = true; runs += 1
           case Markup.FINISHED => runs -= 1

           case Markup.FINALIZED => finalized = true
           case _ =>
         }
       }
       new Command_Status(
+        theory_status = theory_status,
         touched = touched,
         accepted = accepted,
         warned = warned1,
         failed = failed1,
         canceled = canceled,

     def merge(args: IterableOnce[Command_Status]): Command_Status =
       args.iterator.foldLeft(empty)(_ + _)
   }
 
   final class Command_Status private(
+    private val theory_status: Command_Status.Theory_Status.Value,
     private val touched: Boolean,
     private val accepted: Boolean,
     private val warned: Boolean,
     private val failed: Boolean,
     private val canceled: Boolean,

       else if (failed) "Command_Status(failed)"
       else if (warned) "Command_Status(warned)"
       else "Command_Status(...)"
 
     def is_empty: Boolean =
+      !Command_Status.Theory_Status.initialized(theory_status) &&
       !touched && !accepted && !warned && !failed && !canceled && !finalized &&
       forks == 0 && runs == 0
 
     def + (that: Command_Status): Command_Status =
       if (is_empty) that
       else if (that.is_empty) this
       else {
         new Command_Status(
+          theory_status = Command_Status.Theory_Status.merge(theory_status, that.theory_status),
           touched = touched || that.touched,
           accepted = accepted || that.accepted,
           warned = warned || that.warned,
           failed = failed || that.failed,
           canceled = canceled || that.canceled,
           finalized = finalized || that.finalized,
           forks = forks + that.forks,
           runs = runs + that.runs)
       }
+
+    def initialized: Boolean = Command_Status.Theory_Status.initialized(theory_status)
+    def consolidating: Boolean = Command_Status.Theory_Status.consolidating(theory_status)
+    def consolidated: Boolean = Command_Status.Theory_Status.consolidated(theory_status)
+    def maybe_consolidated: Boolean = touched && forks == 0 && runs == 0
 
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     def is_running: Boolean = runs != 0
     def is_warned: Boolean = warned
     def is_failed: Boolean = failed