# HG changeset patch
# User wenzelm
# Date 1376387862 -7200
# Node ID 50d06647cf24d8d83aabfe19e2ccb6b0d3ac522a
# Parent  1f09c98a3232c16f8879148d7bcc415f43839ee0
more cleanup;

diff -r 1f09c98a3232 -r 50d06647cf24 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()
+  }
 }