src/Pure/PIDE/query_operation.scala
changeset 54327 148903e47b26
parent 54325 2c4155003352
child 54640 bbd2fa353809
equal deleted inserted replaced
54326:c5556b404902 54327:148903e47b26
   208   }
   208   }
   209 
   209 
   210   def deactivate() {
   210   def deactivate() {
   211     editor.session.commands_changed -= main_actor
   211     editor.session.commands_changed -= main_actor
   212     remove_overlay()
   212     remove_overlay()
       
   213     reset_state()
       
   214     consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
       
   215     consume_status(current_status)
   213   }
   216   }
   214 }
   217 }