# HG changeset patch # User wenzelm # Date 1285424547 -7200 # Node ID 7c351c1c06245bbafa9a9c6759f4be11561d69a4 # Parent fa55cf2c1ae4e649d3e03e78b74b197be6f32115 simplified / clarified Session.Phase; diff -r fa55cf2c1ae4 -r 7c351c1c0624 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sat Sep 25 15:40:40 2010 +0200 +++ b/src/Pure/System/session.scala Sat Sep 25 16:22:27 2010 +0200 @@ -24,9 +24,10 @@ sealed abstract class Phase case object Inactive extends Phase - case object Startup extends Phase + case object Startup extends Phase // transient + case object Failed extends Phase case object Ready extends Phase - case object Shutdown extends Phase + case object Shutdown extends Phase // transient } @@ -46,7 +47,7 @@ /* pervasive event buses */ - val phase_changed = new Event_Bus[(Session.Phase, Session.Phase)] + val phase_changed = new Event_Bus[Session.Phase] val global_settings = new Event_Bus[Session.Global_Settings.type] val raw_messages = new Event_Bus[Isabelle_Process.Result] val commands_changed = new Event_Bus[Session.Commands_Changed] @@ -126,9 +127,8 @@ def phase = _phase private def phase_=(new_phase: Session.Phase) { - val old_phase = _phase _phase = new_phase - phase_changed.event(old_phase, new_phase) + phase_changed.event(new_phase) } private val global_state = new Volatile(Document.State.init) @@ -209,6 +209,7 @@ if (result.is_syslog) { reverse_syslog ::= result.message if (result.is_ready) phase = Session.Ready + else if (result.is_exit && phase == Session.Startup) phase = Session.Failed else if (result.is_exit) phase = Session.Inactive } else if (result.is_stdout) { } @@ -257,14 +258,18 @@ 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 + if (phase == Session.Inactive || phase == Session.Failed) { + 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 - prover.terminate - phase = Session.Inactive + case Stop => + if (phase == Session.Ready) { + global_state.change(_ => Document.State.init) // FIXME event bus!? + phase = Session.Shutdown + prover.terminate + phase = Session.Inactive + } finished = true reply(()) diff -r fa55cf2c1ae4 -r 7c351c1c0624 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Sat Sep 25 15:40:40 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Sat Sep 25 16:22:27 2010 +0200 @@ -212,16 +212,14 @@ private def start_session() { - if (Isabelle.session.phase == Session.Inactive) { - val timeout = Isabelle.Int_Property("startup-timeout") max 1000 - val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) - val logic = { - val logic = Isabelle.Property("logic") - if (logic != null && logic != "") logic - else Isabelle.default_logic() - } - Isabelle.session.start(timeout, modes ::: List(logic)) + val timeout = Isabelle.Int_Property("startup-timeout") max 1000 + val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) + val logic = { + val logic = Isabelle.Property("logic") + if (logic != null && logic != "") logic + else Isabelle.default_logic() } + Isabelle.session.start(timeout, modes ::: List(logic)) } private def init_model(buffer: Buffer): Option[Document_Model] = @@ -262,14 +260,13 @@ private val session_manager = actor { loop { react { - case (Session.Startup, Session.Inactive) => + case Session.Failed => val text = new scala.swing.TextArea(Isabelle.session.syslog()) text.editable = false Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) - case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer) - case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer) - + case Session.Ready => Isabelle.jedit_buffers.foreach(activate_buffer) + case Session.Shutdown => Isabelle.jedit_buffers.foreach(deactivate_buffer) case _ => } } @@ -284,14 +281,14 @@ case msg: EditorStarted => start_session() case msg: BufferUpdate - if Isabelle.session.phase == Session.Ready && + if Isabelle.session.phase == Session.Ready && // FIXME race!? msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => val buffer = msg.getBuffer if (buffer != null) activate_buffer(buffer) case msg: EditPaneUpdate - if Isabelle.session.phase == Session.Ready && + if Isabelle.session.phase == Session.Ready && // FIXME race!? (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || msg.getWhat == EditPaneUpdate.CREATED || diff -r fa55cf2c1ae4 -r 7c351c1c0624 src/Tools/jEdit/src/jedit/session_dockable.scala --- a/src/Tools/jEdit/src/jedit/session_dockable.scala Sat Sep 25 15:40:40 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Sat Sep 25 16:22:27 2010 +0200 @@ -79,7 +79,7 @@ } } - case (_, phase: Session.Phase) => + case phase: Session.Phase => Swing_Thread.now { session_phase.text = " " + phase.toString + " " } case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)