src/Pure/System/session.scala
changeset 39701 7c351c1c0624
parent 39698 625a3bc4417b
child 40478 4bae781b8f7c
     1.1 --- a/src/Pure/System/session.scala	Sat Sep 25 15:40:40 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Sep 25 16:22:27 2010 +0200
     1.3 @@ -24,9 +24,10 @@
     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 Startup extends Phase  // transient
     1.9 +  case object Failed extends Phase
    1.10    case object Ready extends Phase
    1.11 -  case object Shutdown extends Phase
    1.12 +  case object Shutdown extends Phase  // transient
    1.13  }
    1.14  
    1.15  
    1.16 @@ -46,7 +47,7 @@
    1.17  
    1.18    /* pervasive event buses */
    1.19  
    1.20 -  val phase_changed = new Event_Bus[(Session.Phase, Session.Phase)]
    1.21 +  val phase_changed = new Event_Bus[Session.Phase]
    1.22    val global_settings = new Event_Bus[Session.Global_Settings.type]
    1.23    val raw_messages = new Event_Bus[Isabelle_Process.Result]
    1.24    val commands_changed = new Event_Bus[Session.Commands_Changed]
    1.25 @@ -126,9 +127,8 @@
    1.26    def phase = _phase
    1.27    private def phase_=(new_phase: Session.Phase)
    1.28    {
    1.29 -    val old_phase = _phase
    1.30      _phase = new_phase
    1.31 -    phase_changed.event(old_phase, new_phase)
    1.32 +    phase_changed.event(new_phase)
    1.33    }
    1.34  
    1.35    private val global_state = new Volatile(Document.State.init)
    1.36 @@ -209,6 +209,7 @@
    1.37            if (result.is_syslog) {
    1.38              reverse_syslog ::= result.message
    1.39              if (result.is_ready) phase = Session.Ready
    1.40 +            else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
    1.41              else if (result.is_exit) phase = Session.Inactive
    1.42            }
    1.43            else if (result.is_stdout) { }
    1.44 @@ -257,14 +258,18 @@
    1.45          case result: Isabelle_Process.Result => handle_result(result)
    1.46  
    1.47          case Start(timeout, args) if prover == null =>
    1.48 -          phase = Session.Startup
    1.49 -          prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
    1.50 +          if (phase == Session.Inactive || phase == Session.Failed) {
    1.51 +            phase = Session.Startup
    1.52 +            prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
    1.53 +          }
    1.54  
    1.55 -        case Stop if phase == Session.Ready =>
    1.56 -          global_state.change(_ => Document.State.init)  // FIXME event bus!?
    1.57 -          phase = Session.Shutdown
    1.58 -          prover.terminate
    1.59 -          phase = Session.Inactive
    1.60 +        case Stop =>
    1.61 +          if (phase == Session.Ready) {
    1.62 +            global_state.change(_ => Document.State.init)  // FIXME event bus!?
    1.63 +            phase = Session.Shutdown
    1.64 +            prover.terminate
    1.65 +            phase = Session.Inactive
    1.66 +          }
    1.67            finished = true
    1.68            reply(())
    1.69