src/Pure/PIDE/query_operation.scala
changeset 54327 148903e47b26
parent 54325 2c4155003352
child 54640 bbd2fa353809
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Fri Oct 11 22:11:07 2013 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Fri Oct 11 23:12:04 2013 +0200
     1.3 @@ -210,5 +210,8 @@
     1.4    def deactivate() {
     1.5      editor.session.commands_changed -= main_actor
     1.6      remove_overlay()
     1.7 +    reset_state()
     1.8 +    consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
     1.9 +    consume_status(current_status)
    1.10    }
    1.11  }