src/Pure/PIDE/query_operation.scala
changeset 54310 6ddeb83eb67a
parent 53872 6e69f9ca8f1c
child 54325 2c4155003352
     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      }