tuned signature;

--- a/src/Pure/PIDE/document.scala	Tue Sep 16 10:39:53 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 16 11:23:50 2025 +0200
@@ -1267,6 +1267,10 @@
       self.map(_._2) ::: others.flatMap(_.redirect(command))
     }
 
+    def command_status(version: Version, command: Command): Document_Status.Command_Status =
+      Document_Status.Command_Status.merge(
+        command_states(version, command).iterator.map(_.document_status))
+
     def command_results(version: Version, command: Command): Command.Results =
       Command.State.merge_results(command_states(version, command))
 

--- a/src/Pure/PIDE/document_status.scala	Tue Sep 16 10:39:53 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala	Tue Sep 16 11:23:50 2025 +0200
@@ -168,8 +168,7 @@
       var terminated = true
       var finalized = false
       for (command <- node.commands.iterator) {
-        val states = state.command_states(version, command)
-        val status = Command_Status.merge(states.iterator.map(_.document_status))
+        val status = state.command_status(version, command)
 
         if (status.is_running) running += 1
         else if (status.is_failed) failed += 1