--- 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