# HG changeset patch
# User wenzelm
# Date 1497711711 -7200
# Node ID 8b433b6f302f727b9991930fa8af05f1b8b2fa59
# Parent  8c8e77dbe6fec6b1bf09d272b55d8ef98e8f0280
more permissive: avoid situations where query is silently ignored;

diff -r 8c8e77dbe6fe -r 8b433b6f302f 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 =>