# HG changeset patch
# User wenzelm
# Date 1446485517 -3600
# Node ID 8494a947fa656e74eabc48eb1502c9a0cf3c69c8
# Parent  53bb4172c7f7611956adbf2dae95c7daa47543fd
avoid premature flushing and thus flashing of text area;

diff -r 53bb4172c7f7 -r 8494a947fa65 src/Pure/PIDE/query_operation.scala
--- 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()
-          }
         }
       }
     }