clarified signature: more explicit type Progress.Nodes_Status;

--- a/src/Pure/Build/build_job.scala	Mon Sep 22 16:19:39 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Mon Sep 22 16:43:53 2025 +0200
@@ -240,9 +240,9 @@
                 val updated = nodes_status1 != nodes_status
                 nodes_changed = Set.empty
                 nodes_status = nodes_status1
-                if (updated) Some (nodes_status1) else None
+                if (updated) Some(Progress.Nodes_Status(nodes_domain, nodes_status1)) else None
               }
-            result.foreach(progress.nodes_status(nodes_domain, _))
+            result.foreach(progress.nodes_status)
           }
 
           val nodes_delay = Delay.first(build_progress_delay) { nodes_status_progress() }

--- a/src/Pure/Build/database_progress.scala	Mon Sep 22 16:19:39 2025 +0200
+++ b/src/Pure/Build/database_progress.scala	Mon Sep 22 16:43:53 2025 +0200
@@ -311,10 +311,8 @@
   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(
-    domain: List[Document.Node.Name],
-    nodes_status: Document_Status.Nodes_Status
-  ): Unit = base_progress.nodes_status(domain, nodes_status)
+  override def nodes_status(nodes_status: Progress.Nodes_Status): Unit =
+    base_progress.nodes_status(nodes_status)
 
   override def verbose: Boolean = base_progress.verbose
 

--- a/src/Pure/PIDE/headless.scala	Mon Sep 22 16:19:39 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 22 16:43:53 2025 +0200
@@ -352,7 +352,8 @@
         val delay_nodes_status =
           Delay.first(nodes_status_delay max Time.zero) {
             val st = use_theories_state.value
-            progress.nodes_status(st.dep_graph.topological_order, st.nodes_status)
+            progress.nodes_status(
+              Progress.Nodes_Status(st.dep_graph.topological_order, st.nodes_status))
           }
 
         val delay_commit_clean =

--- a/src/Pure/System/progress.scala	Mon Sep 22 16:19:39 2025 +0200
+++ b/src/Pure/System/progress.scala	Mon Sep 22 16:43:53 2025 +0200
@@ -46,6 +46,13 @@
     def print_percentage: String =
       percentage match { case None => "" case Some(p) => " " + p + "%" }
   }
+
+  sealed case class Nodes_Status(
+    domain: List[Document.Node.Name],
+    document_status: Document_Status.Nodes_Status
+  ) {
+    def apply(name: Document.Node.Name): Document_Status.Node_Status = document_status(name)
+  }
 }
 
 class Progress {
@@ -67,9 +74,7 @@
   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(
-    domain: List[Document.Node.Name],
-    nodes_status: Document_Status.Nodes_Status): Unit = {}
+  def nodes_status(nodes_status: Progress.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	Mon Sep 22 16:19:39 2025 +0200
+++ b/src/Pure/Tools/server.scala	Mon Sep 22 16:43:53 2025 +0200
@@ -274,13 +274,10 @@
       context.writeln(theory.message.text, entries ::: more.toList:_*)
     }
 
-    override def nodes_status(
-      domain: List[Document.Node.Name],
-      nodes_status: Document_Status.Nodes_Status
-    ): Unit = {
+    override def nodes_status(nodes_status: Progress.Nodes_Status): Unit = {
       val json =
         List.from(for {
-          name <- domain.iterator
+          name <- nodes_status.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))