# HG changeset patch
# User wenzelm
# Date 1381525924 -7200
# Node ID 148903e47b26adb0eab28f8df23574e7e94e89e7
# Parent  c5556b404902c34d56662ea52c3fbbaa2241e343
more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;

diff -r c5556b404902 -r 148903e47b26 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Fri Oct 11 22:11:07 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Fri Oct 11 23:12:04 2013 +0200
@@ -210,5 +210,8 @@
   def deactivate() {
     editor.session.commands_changed -= main_actor
     remove_overlay()
+    reset_state()
+    consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+    consume_status(current_status)
   }
 }