# 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() - } } } }