src/Pure/PIDE/document_status.scala
changeset 83164 851f3f9440ef
parent 83163 64c9d94478b8
child 83165 9f3f723938fc
--- 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