src/Pure/PIDE/query_operation.scala
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()
+  }
 }