# HG changeset patch
# User wenzelm
# Date 1757968564 -7200
# Node ID 7e94f31b6d6c41d758736fbee2e7c1c53b532448
# Parent  dc54c60492c3b15bd20f039ec2f14d9bfa610785
clarified signature: more explicit type Theory_Status;
minor performance tuning;

diff -r dc54c60492c3 -r 7e94f31b6d6c src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Sep 15 18:09:55 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Sep 15 22:36:04 2025 +0200
@@ -213,30 +213,15 @@
     exports: Exports = Exports.empty,
     markups: Markups = Markups.empty
   ) {
-    lazy val initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
-    lazy val consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING)
-    lazy val consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED)
-
-    lazy val maybe_consolidated: Boolean = {
-      var touched = false
-      var forks = 0
-      var runs = 0
-      for (markup <- status) {
-        markup.name match {
-          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 _ =>
-        }
-      }
-      touched && forks == 0 && runs == 0
-    }
-
     lazy val document_status: Document_Status.Command_Status =
       Document_Status.Command_Status.make(
         status, warned = results.warned, failed = results.failed)
 
+    def initialized: Boolean = document_status.initialized
+    def consolidating: Boolean = document_status.consolidating
+    def consolidated: Boolean = document_status.consolidated
+    def maybe_consolidated: Boolean = document_status.maybe_consolidated
+
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
     def redirect(other_command: Command): Option[State] = {
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