--- 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*)