simplified / clarified Session.Phase;

--- 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(())
 

--- 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 ||

--- 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)