src/Pure/PIDE/query_operation.scala
changeset 53000 50d06647cf24
parent 52981 c7afd884dfb2
child 53840 75243ba102d4
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Tue Aug 13 11:49:01 2013 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Tue Aug 13 11:57:42 2013 +0200
     1.3 @@ -199,5 +199,9 @@
     1.4    }
     1.5  
     1.6    def activate() { editor.session.commands_changed += main_actor }
     1.7 -  def deactivate() { editor.session.commands_changed -= main_actor }
     1.8 +
     1.9 +  def deactivate() {
    1.10 +    editor.session.commands_changed -= main_actor
    1.11 +    remove_overlay()
    1.12 +  }
    1.13  }