1.1 --- a/src/Pure/System/session.scala	Thu Sep 23 22:00:36 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu Sep 23 22:04:18 2010 +0200
     1.3 @@ -24,11 +24,9 @@
     1.4  
     1.5    sealed abstract class Phase
     1.6    case object Inactive extends Phase
     1.7 -  case object Startup extends Phase
     1.8    case object Exit extends Phase
     1.9    case object Ready extends Phase
    1.10    case object Shutdown extends Phase
    1.11 -  case object Terminated extends Phase
    1.12  }
    1.13  
    1.14  
    1.15 @@ -126,7 +124,7 @@
    1.16  
    1.17    @volatile private var _phase: Session.Phase = Session.Inactive
    1.18    def phase = _phase
    1.19 -  def phase_=(new_phase: Session.Phase)
    1.20 +  private def phase_=(new_phase: Session.Phase)
    1.21    {
    1.22      val old_phase = _phase
    1.23      _phase = new_phase
    1.24 @@ -211,7 +209,10 @@
    1.25            if (result.is_syslog) {
    1.26              reverse_syslog ::= result.message
    1.27              if (result.is_ready) phase = Session.Ready
    1.28 -            else if (result.is_exit) phase = Session.Exit
    1.29 +            else if (result.is_exit) {
    1.30 +              phase = Session.Exit
    1.31 +              phase = Session.Inactive
    1.32 +            }
    1.33            }
    1.34            else if (result.is_stdout) { }
    1.35            else if (result.is_status) {
    1.36 @@ -259,14 +260,13 @@
    1.37          case result: Isabelle_Process.Result => handle_result(result)
    1.38  
    1.39          case Start(timeout, args) if prover == null =>
    1.40 -          phase = Session.Startup
    1.41            prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
    1.42  
    1.43          case Stop if phase == Session.Ready =>
    1.44            global_state.change(_ => Document.State.init)  // FIXME event bus!?
    1.45            phase = Session.Shutdown
    1.46            prover.terminate
    1.47 -          phase = Session.Terminated
    1.48 +          phase = Session.Inactive
    1.49            finished = true
    1.50            reply(())
    1.51