# HG changeset patch
# User wenzelm
# Date 1535221320 -7200
# Node ID e28978310a2addaa6e3adee0163ac86241ea14c8
# Parent  4597812d518231883efc7ecf1d1b5c68e428f73c
more robust exit: avoid later Consolidate_Execution with handle_raw_edits (cf. 2fd3a6d6ba2e);

diff -r 4597812d5182 -r e28978310a2a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Aug 25 20:10:49 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Aug 25 20:22:00 2018 +0200
@@ -307,18 +307,25 @@
     private val delay =
       Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
 
-    private val changed_nodes = Synchronized(Set.empty[Document.Node.Name])
+    private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
+    private val state = Synchronized(init_state)
+
+    def exit()
+    {
+      delay.revoke()
+      state.change(_ => None)
+    }
 
     def update(new_nodes: Set[Document.Node.Name] = Set.empty)
     {
-      changed_nodes.change(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)
-      delay.invoke()
+      val active =
+        state.change_result(st =>
+          (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
+      if (active) delay.invoke()
     }
 
     def flush(): Set[Document.Node.Name] =
-      changed_nodes.change_result(nodes => (nodes, Set.empty))
-
-    def revoke() { delay.revoke() }
+      state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None))
   }
 
 
@@ -549,7 +556,7 @@
             prover.set(start_prover(manager.send(_)))
 
           case Stop =>
-            consolidation.revoke()
+            consolidation.exit()
             delay_prune.revoke()
             if (prover.defined) {
               protocol_handlers.exit()