# HG changeset patch
# User wenzelm
# Date 1451935394 -3600
# Node ID 644a2eed86331c7bec00c0b0e028ca289aa3d4eb
# Parent  fefd79f6b232def7b188f1337229ac293c78cb35
clarified order of shutdown;

diff -r fefd79f6b232 -r 644a2eed8633 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Jan 03 21:45:34 2016 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Jan 04 20:23:14 2016 +0100
@@ -605,11 +605,11 @@
 
   def stop()
   {
+    delay_prune.revoke()
     manager.send_wait(Stop)
     prover.await_reset()
     change_parser.shutdown()
     change_buffer.shutdown()
-    delay_prune.revoke()
     manager.shutdown()
     dispatcher.shutdown()
   }