--- a/src/Pure/PIDE/query_operation.scala Thu Oct 23 14:49:21 2025 +0200
+++ b/src/Pure/PIDE/query_operation.scala Thu Oct 23 16:15:40 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.require_dispatcher {}
+ editor.send_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,9 +182,10 @@
case None =>
}
- consume_status(current_state.value.status)
- editor.flush()
- case None =>
+ consume_status(current_state.value.status)
+ editor.flush()
+ case None =>
+ }
}
}