changeset 53000 | 50d06647cf24 |
parent 52981 | c7afd884dfb2 |
child 53840 | 75243ba102d4 |
--- a/src/Pure/PIDE/query_operation.scala Tue Aug 13 11:49:01 2013 +0200 +++ b/src/Pure/PIDE/query_operation.scala Tue Aug 13 11:57:42 2013 +0200 @@ -199,5 +199,9 @@ } def activate() { editor.session.commands_changed += main_actor } - def deactivate() { editor.session.commands_changed -= main_actor } + + def deactivate() { + editor.session.commands_changed -= main_actor + remove_overlay() + } }