simplified / clarified Session.Phase;
authorwenzelm
Sat Sep 25 16:22:27 2010 +0200 (2010-09-25)
changeset 397017c351c1c0624
parent 39700 fa55cf2c1ae4
child 39702 d7c256cb2797
simplified / clarified Session.Phase;
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/plugin.scala
src/Tools/jEdit/src/jedit/session_dockable.scala
     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  
     2.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 25 15:40:40 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 25 16:22:27 2010 +0200
     2.3 @@ -212,16 +212,14 @@
     2.4  
     2.5    private def start_session()
     2.6    {
     2.7 -    if (Isabelle.session.phase == Session.Inactive) {
     2.8 -      val timeout = Isabelle.Int_Property("startup-timeout") max 1000
     2.9 -      val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    2.10 -      val logic = {
    2.11 -        val logic = Isabelle.Property("logic")
    2.12 -        if (logic != null && logic != "") logic
    2.13 -        else Isabelle.default_logic()
    2.14 -      }
    2.15 -      Isabelle.session.start(timeout, modes ::: List(logic))
    2.16 +    val timeout = Isabelle.Int_Property("startup-timeout") max 1000
    2.17 +    val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    2.18 +    val logic = {
    2.19 +      val logic = Isabelle.Property("logic")
    2.20 +      if (logic != null && logic != "") logic
    2.21 +      else Isabelle.default_logic()
    2.22      }
    2.23 +    Isabelle.session.start(timeout, modes ::: List(logic))
    2.24    }
    2.25  
    2.26    private def init_model(buffer: Buffer): Option[Document_Model] =
    2.27 @@ -262,14 +260,13 @@
    2.28    private val session_manager = actor {
    2.29      loop {
    2.30        react {
    2.31 -        case (Session.Startup, Session.Inactive) =>
    2.32 +        case Session.Failed =>
    2.33            val text = new scala.swing.TextArea(Isabelle.session.syslog())
    2.34            text.editable = false
    2.35            Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
    2.36  
    2.37 -        case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer)
    2.38 -        case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer)
    2.39 -
    2.40 +        case Session.Ready => Isabelle.jedit_buffers.foreach(activate_buffer)
    2.41 +        case Session.Shutdown => Isabelle.jedit_buffers.foreach(deactivate_buffer)
    2.42          case _ =>
    2.43        }
    2.44      }
    2.45 @@ -284,14 +281,14 @@
    2.46        case msg: EditorStarted => start_session()
    2.47  
    2.48        case msg: BufferUpdate
    2.49 -      if Isabelle.session.phase == Session.Ready &&
    2.50 +      if Isabelle.session.phase == Session.Ready &&  // FIXME race!?
    2.51          msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
    2.52  
    2.53          val buffer = msg.getBuffer
    2.54          if (buffer != null) activate_buffer(buffer)
    2.55  
    2.56        case msg: EditPaneUpdate
    2.57 -      if Isabelle.session.phase == Session.Ready &&
    2.58 +      if Isabelle.session.phase == Session.Ready &&  // FIXME race!?
    2.59          (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
    2.60            msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    2.61            msg.getWhat == EditPaneUpdate.CREATED ||
     3.1 --- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Sat Sep 25 15:40:40 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Sat Sep 25 16:22:27 2010 +0200
     3.3 @@ -79,7 +79,7 @@
     3.4                }
     3.5              }
     3.6  
     3.7 -        case (_, phase: Session.Phase) =>
     3.8 +        case phase: Session.Phase =>
     3.9            Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
    3.10  
    3.11          case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)