more permissive: avoid situations where query is silently ignored;
authorwenzelm
Sat, 17 Jun 2017 17:01:51 +0200
changeset 66108 8b433b6f302f
parent 66107 8c8e77dbe6fe
child 66111 20304512a33b
more permissive: avoid situations where query is silently ignored;
src/Pure/PIDE/query_operation.scala
--- 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 =>