--- a/src/Pure/PIDE/query_operation.scala Fri Oct 11 12:06:26 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala Fri Oct 11 20:45:21 2013 +0200
@@ -155,13 +155,15 @@
remove_overlay()
reset_state()
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
- editor.current_command(editor_context, snapshot) match {
- case Some(command) =>
- current_location = Some(command)
- current_query = query
- current_status = Query_Operation.Status.WAITING
- editor.insert_overlay(command, operation_name, instance :: query)
- case None =>
+ if (!snapshot.is_outdated) {
+ editor.current_command(editor_context, snapshot) match {
+ case Some(command) =>
+ current_location = Some(command)
+ current_query = query
+ current_status = Query_Operation.Status.WAITING
+ editor.insert_overlay(command, operation_name, instance :: query)
+ case None =>
+ }
}
consume_status(current_status)
editor.flush()