# HG changeset patch
# User wenzelm
# Date 1381141699 -7200
# Node ID 6ddeb83eb67ae812ea61816b02b276a435859248
# Parent  626e42d9b9edcc885d5aeda921761843d30b1671
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;

diff -r 626e42d9b9ed -r 6ddeb83eb67a src/Pure/PIDE/query_operation.scala
--- 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()
-          }
         }
       }
     }