author | wenzelm |
Tue, 13 Aug 2013 11:57:42 +0200 | |
changeset 53000 | 50d06647cf24 |
parent 52999 | 1f09c98a3232 |
child 53001 | 0ef4699b2502 |
--- 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() + } }