# HG changeset patch
# User wenzelm
# Date 1528209352 -7200
# Node ID b10ae73f0bab73e0ef15ef6d6e7a43fcec478581
# Parent  2fd3a6d6ba2e455601fd80a4d66e2d6b9a0315e3
more robust;

diff -r 2fd3a6d6ba2e -r b10ae73f0bab src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Jun 05 16:12:26 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Jun 05 16:35:52 2018 +0200
@@ -318,7 +318,7 @@
     def flush(): Set[Document.Node.Name] =
       changed_nodes.change_result(nodes => (nodes, Set.empty))
 
-    def shutdown() { delay.revoke() }
+    def revoke() { delay.revoke() }
   }
 
 
@@ -549,6 +549,7 @@
             prover.set(start_prover(manager.send(_)))
 
           case Stop =>
+            consolidation.revoke()
             delay_prune.revoke()
             if (prover.defined) {
               protocol_handlers.exit()
@@ -654,7 +655,6 @@
 
     change_parser.shutdown()
     change_buffer.shutdown()
-    consolidation.shutdown()
     manager.shutdown()
     dispatcher.shutdown()