diff -r 166196bdda3c -r 182728f4e18b src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Sun Oct 26 21:36:08 2025 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Mon Oct 27 10:33:53 2025 +0100
@@ -71,10 +71,11 @@
           val snapshot = editor.node_snapshot(cmd.node_name)
           val command_results = snapshot.command_results(cmd)
           val results =
-            (for {
-              case (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
-              if props.contains((Markup.INSTANCE, state0.instance))
-            } yield elem).toList
+            List.from(
+              for {
+                case (_, elem@XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
+                if props.contains((Markup.INSTANCE, state0.instance))
+              } yield elem)
           val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd)
           (snapshot, command_results, results, removed)
         case None =>
@@ -141,8 +142,9 @@
       }).foreach(id => current_state.change(_.copy(exec_id = id)))
 
     if (state0.output != new_output || state0.status != new_status) {
-      if (snapshot.is_outdated)
+      if (snapshot.is_outdated) {
         current_state.change(_.copy(update_pending = true))
+      }
       else {
         current_state.change(_.copy(update_pending = false))
         if (state0.output != new_output && !removed) {