more cleanup;
authorwenzelm
Tue, 13 Aug 2013 11:57:42 +0200
changeset 53000 50d06647cf24
parent 52999 1f09c98a3232
child 53001 0ef4699b2502
more cleanup;
src/Pure/PIDE/query_operation.scala
--- 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()
+  }
 }