diff -r dc54c60492c3 -r 7e94f31b6d6c src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Mon Sep 15 18:09:55 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Mon Sep 15 22:36:04 2025 +0200
@@ -11,6 +11,16 @@
   /* 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)
@@ -23,6 +33,7 @@
       warned: Boolean = false,
       failed: Boolean = false
     ): Command_Status = {
+      var theory_status = Theory_Status.NONE
       var touched = false
       var accepted = false
       var warned1 = warned
@@ -33,6 +44,12 @@
       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
@@ -46,6 +63,7 @@
         }
       }
       new Command_Status(
+        theory_status = theory_status,
         touched = touched,
         accepted = accepted,
         warned = warned1,
@@ -63,6 +81,7 @@
   }
 
   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,
@@ -79,6 +98,7 @@
       else "Command_Status(...)"
 
     def is_empty: Boolean =
+      !Command_Status.Theory_Status.initialized(theory_status) &&
       !touched && !accepted && !warned && !failed && !canceled && !finalized &&
       forks == 0 && runs == 0
 
@@ -87,6 +107,7 @@
       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,
@@ -97,6 +118,11 @@
           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