more uniform Command_Status.theory_status vs. Node_Status.theory_status: cover all command_states, without special cases;

--- a/src/Pure/PIDE/command.scala	Tue Sep 16 11:23:50 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 16 11:58:46 2025 +0200
@@ -464,8 +464,6 @@
   lazy val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
   lazy val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
 
-  def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
-
 
   /* blobs */
 

--- a/src/Pure/PIDE/document.scala	Tue Sep 16 11:23:50 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 16 11:58:46 2025 +0200
@@ -1312,13 +1312,6 @@
       else Nil
     }
 
-    def node_initialized(version: Version, name: Node.Name): Boolean =
-      name.is_theory &&
-      (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
-        case None => false
-        case Some(command) => command_states(version, command).headOption.exists(_.initialized)
-      })
-
     def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
       name.is_theory &&
       version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _))

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 11:23:50 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 16 11:58:46 2025 +0200
@@ -21,6 +21,14 @@
     def merge(t1: Value, t2: Value): Value = if (t1 >= t2) t1 else t2
   }
 
+  trait Theory_Status {
+    def theory_status: Theory_Status.Value
+    def initialized: Boolean = Theory_Status.initialized(theory_status)
+    def finalized: Boolean = Theory_Status.finalized(theory_status)
+    def consolidating: Boolean = Theory_Status.consolidating(theory_status)
+    def consolidated: Boolean = Theory_Status.consolidated(theory_status)
+  }
+
 
   /* command status */
 
@@ -84,7 +92,7 @@
   }
 
   final class Command_Status private(
-    private val theory_status: Theory_Status.Value,
+    val theory_status: Theory_Status.Value,
     private val touched: Boolean,
     private val accepted: Boolean,
     private val warned: Boolean,
@@ -92,7 +100,7 @@
     private val canceled: Boolean,
     val forks: Int,
     val runs: Int
-  ) {
+  ) extends Theory_Status {
     override def toString: String =
       if (is_empty) "Command_Status.empty"
       else if (failed) "Command_Status(failed)"
@@ -119,10 +127,6 @@
           runs = runs + that.runs)
       }
 
-    def initialized: Boolean = Theory_Status.initialized(theory_status)
-    def finalized: Boolean = Theory_Status.finalized(theory_status)
-    def consolidating: Boolean = Theory_Status.consolidating(theory_status)
-    def consolidated: Boolean = 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))
@@ -148,9 +152,7 @@
         finished = 0,
         canceled = false,
         terminated = false,
-        initialized = false,
-        finalized = false,
-        consolidated = false)
+        theory_status = Document_Status.Theory_Status.NONE)
 
     def make(
       state: Document.State,
@@ -166,7 +168,7 @@
       var finished = 0
       var canceled = false
       var terminated = true
-      var finalized = false
+      var theory_status = Document_Status.Theory_Status.NONE
       for (command <- node.commands.iterator) {
         val status = state.command_status(version, command)
 
@@ -178,10 +180,9 @@
 
         if (status.is_canceled) canceled = true
         if (!status.is_terminated) terminated = false
-        if (status.finalized) finalized = true
+
+        theory_status = Theory_Status.merge(theory_status, status.theory_status)
       }
-      val initialized = state.node_initialized(version, name)
-      val consolidated = state.node_consolidated(version, name)
 
       Node_Status(
         suppressed = version.nodes.suppressed(name),
@@ -192,9 +193,7 @@
         finished = finished,
         canceled = canceled,
         terminated = terminated,
-        initialized = initialized,
-        finalized = finalized,
-        consolidated = consolidated)
+        theory_status = theory_status)
     }
   }
 
@@ -207,10 +206,8 @@
     finished: Int,
     canceled: Boolean,
     terminated: Boolean,
-    initialized: Boolean,
-    finalized: Boolean,
-    consolidated: Boolean
-  ) {
+    theory_status: Theory_Status.Value
+  ) extends Theory_Status {
     def is_empty: Boolean = this == Node_Status.empty
 
     def ok: Boolean = failed == 0