author | wenzelm |
Fri, 11 Oct 2013 23:12:04 +0200 | |
changeset 54327 | 148903e47b26 |
parent 54326 | c5556b404902 |
child 54328 | ffa4e0b1701e |
--- a/src/Pure/PIDE/query_operation.scala Fri Oct 11 22:11:07 2013 +0200 +++ b/src/Pure/PIDE/query_operation.scala Fri Oct 11 23:12:04 2013 +0200 @@ -210,5 +210,8 @@ def deactivate() { editor.session.commands_changed -= main_actor remove_overlay() + reset_state() + consume_output(Document.Snapshot.init, Command.Results.empty, Nil) + consume_status(current_status) } }