--- a/src/Pure/PIDE/query_operation.scala Sat Jun 17 16:36:45 2017 +0200
+++ b/src/Pure/PIDE/query_operation.scala Sat Jun 17 17:01:51 2017 +0200
@@ -185,15 +185,15 @@
remove_overlay()
current_state.change(_ => Query_Operation.State.empty)
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
- if (!snapshot.is_outdated) {
- editor.current_command(editor_context, snapshot) match {
- case Some(command) =>
- val state = Query_Operation.State.make(command, query)
- current_state.change(_ => state)
- editor.insert_overlay(command, print_function, state.instance :: query)
- case None =>
- }
+
+ editor.current_command(editor_context, snapshot) match {
+ case Some(command) =>
+ val state = Query_Operation.State.make(command, query)
+ current_state.change(_ => state)
+ editor.insert_overlay(command, print_function, state.instance :: query)
+ case None =>
}
+
consume_status(current_state.value.status)
editor.flush()
case None =>