# HG changeset patch
# User wenzelm
# Date 1489415539 -3600
# Node ID eb89ad5ae115fed5f7cab97a9d83f7573eb03135
# Parent  91c528cd376ab5dd241d93d6f2ec4a014ecd61d7
tuned signature;

diff -r 91c528cd376a -r eb89ad5ae115 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Mar 13 15:25:25 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Mon Mar 13 15:32:19 2017 +0100
@@ -609,7 +609,7 @@
       })
   }
 
-  def stop()
+  def stop(): Int =
   {
     val was_ready =
       _phase.guarded_access(phase =>
@@ -626,6 +626,11 @@
     change_buffer.shutdown()
     manager.shutdown()
     dispatcher.shutdown()
+
+    phase match {
+      case Session.Terminated(rc) => rc
+      case phase => error("Bad session phase after shutdown: " + quote(phase.print))
+    }
   }
 
   def protocol_command(name: String, args: String*)