src/Pure/PIDE/query_operation.scala

--- a/src/Pure/PIDE/query_operation.scala	Thu Oct 23 16:37:18 2025 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Thu Oct 23 16:52:05 2025 +0200
@@ -166,13 +166,13 @@
     editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) }
 
   def apply_query(query: List[String]): Unit = {
-    editor.send_dispatcher {
+    editor.require_dispatcher {}
 
-      editor.current_node_snapshot(editor_context) match {
-        case Some(snapshot) =>
-          remove_overlay()
-          current_state.change(_ => Query_Operation.State.empty)
-          consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+    editor.current_node_snapshot(editor_context) match {
+      case Some(snapshot) =>
+        remove_overlay()
+        current_state.change(_ => Query_Operation.State.empty)
+        consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
 
         editor.current_command(editor_context, snapshot) match {
           case Some(command) =>
@@ -182,10 +182,9 @@
           case None =>
         }
 
-          consume_status(current_state.value.status)
-          editor.flush()
-        case None =>
-      }
+        consume_status(current_state.value.status)
+        editor.flush()
+      case None =>
     }
   }