src/Pure/PIDE/query_operation.scala
changeset 54325 2c4155003352
parent 54310 6ddeb83eb67a
child 54327 148903e47b26
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Fri Oct 11 12:06:26 2013 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Fri Oct 11 20:45:21 2013 +0200
     1.3 @@ -155,13 +155,15 @@
     1.4          remove_overlay()
     1.5          reset_state()
     1.6          consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
     1.7 -        editor.current_command(editor_context, snapshot) match {
     1.8 -          case Some(command) =>
     1.9 -            current_location = Some(command)
    1.10 -            current_query = query
    1.11 -            current_status = Query_Operation.Status.WAITING
    1.12 -            editor.insert_overlay(command, operation_name, instance :: query)
    1.13 -          case None =>
    1.14 +        if (!snapshot.is_outdated) {
    1.15 +          editor.current_command(editor_context, snapshot) match {
    1.16 +            case Some(command) =>
    1.17 +              current_location = Some(command)
    1.18 +              current_query = query
    1.19 +              current_status = Query_Operation.Status.WAITING
    1.20 +              editor.insert_overlay(command, operation_name, instance :: query)
    1.21 +            case None =>
    1.22 +          }
    1.23          }
    1.24          consume_status(current_status)
    1.25          editor.flush()