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;
1.1 --- a/src/Pure/PIDE/query_operation.scala Fri Oct 04 14:35:00 2013 +0200
1.2 +++ b/src/Pure/PIDE/query_operation.scala Mon Oct 07 12:28:19 2013 +0200
1.3 @@ -53,8 +53,12 @@
1.4
1.5 private def remove_overlay()
1.6 {
1.7 - current_location.foreach(command =>
1.8 - editor.remove_overlay(command, operation_name, instance :: current_query))
1.9 + current_location match {
1.10 + case None =>
1.11 + case Some(command) =>
1.12 + editor.remove_overlay(command, operation_name, instance :: current_query)
1.13 + editor.flush()
1.14 + }
1.15 }
1.16
1.17
1.18 @@ -129,10 +133,8 @@
1.19 if (current_status != new_status) {
1.20 current_status = new_status
1.21 consume_status(new_status)
1.22 - if (new_status == Query_Operation.Status.REMOVED) {
1.23 + if (new_status == Query_Operation.Status.REMOVED)
1.24 remove_overlay()
1.25 - editor.flush()
1.26 - }
1.27 }
1.28 }
1.29 }