clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;

--- a/src/Pure/PIDE/query_operation.scala	Fri Oct 04 14:35:00 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Mon Oct 07 12:28:19 2013 +0200
@@ -53,8 +53,12 @@
 
   private def remove_overlay()
   {
-    current_location.foreach(command =>
-      editor.remove_overlay(command, operation_name, instance :: current_query))
+    current_location match {
+      case None =>
+      case Some(command) =>
+        editor.remove_overlay(command, operation_name, instance :: current_query)
+        editor.flush()
+    }
   }
 
 
@@ -129,10 +133,8 @@
         if (current_status != new_status) {
           current_status = new_status
           consume_status(new_status)
-          if (new_status == Query_Operation.Status.REMOVED) {
+          if (new_status == Query_Operation.Status.REMOVED)
             remove_overlay()
-            editor.flush()
-          }
         }
       }
     }