src/Pure/System/session.scala

   case object Assignment
   case class Commands_Changed(set: Set[Command])
 
   sealed abstract class Phase
   case object Inactive extends Phase
-  case object Exit extends Phase
+  case object Startup extends Phase
   case object Ready extends Phase
   case object Shutdown extends Phase
 }
 
 

           catch { case _: Document.State.Fail => bad_result(result) }
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
             if (result.is_ready) phase = Session.Ready
-            else if (result.is_exit) {
-              phase = Session.Exit
-              phase = Session.Inactive
-            }
+            else if (result.is_exit) phase = Session.Inactive
           }
           else if (result.is_stdout) { }
           else if (result.is_status) {
             result.body match {
               case List(Isar_Document.Assign(id, edits)) =>

         case change: Document.Change if prover != null => handle_change(change)
 
         case result: Isabelle_Process.Result => handle_result(result)
 
         case Start(timeout, args) if prover == null =>
+          phase = Session.Startup
           prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
 
         case Stop if phase == Session.Ready =>
           global_state.change(_ => Document.State.init)  // FIXME event bus!?
           phase = Session.Shutdown