clarified signature: explicit domain for Nodes_Status operations;

--- a/src/Pure/Build/database_progress.scala	Sun Sep 21 13:47:47 2025 +0200
+++ b/src/Pure/Build/database_progress.scala	Sun Sep 21 14:22:14 2025 +0200
@@ -311,8 +311,10 @@
   override def output(message: Progress.Message): Unit = sync_context { _consumer.send(message) }
   override def theory(theory: Progress.Theory): Unit = sync_context { _consumer.send(theory) }
 
-  override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
-    base_progress.nodes_status(nodes_status)
+  override def nodes_status(
+    domain: List[Document.Node.Name],
+    nodes_status: Document_Status.Nodes_Status
+  ): Unit = base_progress.nodes_status(domain, nodes_status)
 
   override def verbose: Boolean = base_progress.verbose
 

--- a/src/Pure/PIDE/document_status.scala	Sun Sep 21 13:47:47 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sun Sep 21 14:22:14 2025 +0200
@@ -269,26 +269,15 @@
   enum Overall_Status { case ok, failed, pending }
 
   object Nodes_Status {
-    val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
+    val empty: Nodes_Status = new Nodes_Status(Map.empty)
   }
 
-  final class Nodes_Status private(
-    private val rep: Map[Document.Node.Name, Node_Status],
-    nodes: Document.Nodes
-  ) {
+  final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status]) {
     def is_empty: Boolean = rep.isEmpty
     def apply(name: Document.Node.Name): Node_Status = rep.getOrElse(name, Node_Status.empty)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
-
     def iterator: Iterator[(Document.Node.Name, Node_Status)] = rep.iterator
 
-    def present(
-      domain: Option[List[Document.Node.Name]] = None
-    ): List[(Document.Node.Name, Node_Status)] = {
-      for (name <- domain.getOrElse(nodes.topological_order))
-        yield name -> apply(name)
-    }
-
     def quasi_consolidated(name: Document.Node.Name): Boolean =
       get(name) match {
         case Some(st) => st.quasi_consolidated
@@ -321,7 +310,7 @@
       val rep1 = rep ++ update_iterator
       val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1
 
-      (rep != rep2, new Nodes_Status(rep2, nodes1))
+      (rep != rep2, new Nodes_Status(rep2))
     }
 
     override def hashCode: Int = rep.hashCode

--- a/src/Pure/PIDE/headless.scala	Sun Sep 21 13:47:47 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 21 14:22:14 2025 +0200
@@ -351,7 +351,8 @@
       val consumer = {
         val delay_nodes_status =
           Delay.first(nodes_status_delay max Time.zero) {
-            progress.nodes_status(use_theories_state.value.nodes_status)
+            val st = use_theories_state.value
+            progress.nodes_status(st.dep_graph.topological_order, st.nodes_status)
           }
 
         val delay_commit_clean =
@@ -390,7 +391,8 @@
 
                   val theory_progress =
                     (for {
-                      (name, node_status) <- st1.nodes_status.present().iterator
+                      name <- st1.dep_graph.topological_order.iterator
+                      node_status = st1.nodes_status(name)
                       if !node_status.is_empty && changed_st.changed_nodes(name) &&
                         !st.already_committed.isDefinedAt(name)
                       p1 = node_status.percentage

--- a/src/Pure/System/progress.scala	Sun Sep 21 13:47:47 2025 +0200
+++ b/src/Pure/System/progress.scala	Sun Sep 21 14:22:14 2025 +0200
@@ -67,7 +67,9 @@
   final def echo_if(cond: Boolean, msg: String): Unit = if (cond) echo(msg)
 
   def theory(theory: Progress.Theory): Unit = output(theory.message)
-  def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {}
+  def nodes_status(
+    domain: List[Document.Node.Name],
+    nodes_status: Document_Status.Nodes_Status): Unit = {}
 
   final def capture[A](e: => A, msg: String, err: Throwable => String): Exn.Result[A] = {
     echo(msg)

--- a/src/Pure/Tools/server.scala	Sun Sep 21 13:47:47 2025 +0200
+++ b/src/Pure/Tools/server.scala	Sun Sep 21 14:22:14 2025 +0200
@@ -274,10 +274,15 @@
       context.writeln(theory.message.text, entries ::: more.toList:_*)
     }
 
-    override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {
+    override def nodes_status(
+      domain: List[Document.Node.Name],
+      nodes_status: Document_Status.Nodes_Status
+    ): Unit = {
       val json =
-        for ((name, node_status) <- nodes_status.present() if !node_status.is_empty)
-          yield name.json + ("status" -> node_status.json)
+        List.from(for {
+          name <- domain.iterator
+          node_status = nodes_status(name) if !node_status.is_empty
+        } yield name.json + ("status" -> node_status.json))
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }
 

--- a/src/Tools/jEdit/src/theories_status.scala	Sun Sep 21 13:47:47 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala	Sun Sep 21 14:22:14 2025 +0200
@@ -242,12 +242,11 @@
     nodes_status = nodes_status1
     if (nodes_status_changed || force) {
       gui.listData =
-        if (document) {
-          nodes_status1.present(domain = Some(PIDE.editor.document_theories())).map(_._1)
-        }
+        if (document) PIDE.editor.document_theories()
         else {
           (for {
-            (name, node_status) <- nodes_status1.present().iterator
+            name <- snapshot.version.nodes.topological_order.iterator
+            node_status = nodes_status1(name)
             if !node_status.is_empty && !node_status.suppressed && node_status.total > 0
           } yield name).toList
         }