avoid premature flushing and thus flashing of text area;

--- a/src/Pure/PIDE/query_operation.scala	Mon Nov 02 18:30:25 2015 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Mon Nov 02 18:31:57 2015 +0100
@@ -163,10 +163,8 @@
         if (state0.status != new_status) {
           current_state.change(_.copy(status = new_status))
           consume_status(new_status)
-          if (new_status == Query_Operation.Status.FINISHED) {
+          if (new_status == Query_Operation.Status.FINISHED)
             remove_overlay()
-            editor.flush()
-          }
         }
       }
     }