simplified Session.Phase;
slightly more robust session startup;
misc tuning;

--- a/src/Pure/System/session.scala	Thu Sep 23 22:00:36 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 23 22:04:18 2010 +0200
@@ -24,11 +24,9 @@
 
   sealed abstract class Phase
   case object Inactive extends Phase
-  case object Startup extends Phase
   case object Exit extends Phase
   case object Ready extends Phase
   case object Shutdown extends Phase
-  case object Terminated extends Phase
 }
 
 
@@ -126,7 +124,7 @@
 
   @volatile private var _phase: Session.Phase = Session.Inactive
   def phase = _phase
-  def phase_=(new_phase: Session.Phase)
+  private def phase_=(new_phase: Session.Phase)
   {
     val old_phase = _phase
     _phase = new_phase
@@ -211,7 +209,10 @@
           if (result.is_syslog) {
             reverse_syslog ::= result.message
             if (result.is_ready) phase = Session.Ready
-            else if (result.is_exit) phase = Session.Exit
+            else if (result.is_exit) {
+              phase = Session.Exit
+              phase = Session.Inactive
+            }
           }
           else if (result.is_stdout) { }
           else if (result.is_status) {
@@ -259,14 +260,13 @@
         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
 
         case Stop if phase == Session.Ready =>
           global_state.change(_ => Document.State.init)  // FIXME event bus!?
           phase = Session.Shutdown
           prover.terminate
-          phase = Session.Terminated
+          phase = Session.Inactive
           finished = true
           reply(())
 

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 22:00:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 22:04:18 2010 +0200
@@ -19,7 +19,7 @@
   Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
-import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged, ViewUpdate}
+import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 import org.gjt.sp.util.Log
@@ -210,16 +210,18 @@
 {
   /* session management */
 
-  private def session_startup()
+  private def start_session()
   {
-    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()
+    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))
     }
-    Isabelle.session.start(timeout, modes ::: List(logic))
   }
 
   private def activate_buffer(buffer: Buffer)
@@ -228,9 +230,13 @@
       Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
         case None =>
         case Some((_, thy_name)) =>
-          val model = Document_Model.init(Isabelle.session, buffer, thy_name)
-          for (text_area <- Isabelle.jedit_text_areas(buffer))
-            Document_View.init(model, text_area)
+          if (Document_Model(buffer).isEmpty) {
+            val model = Document_Model.init(Isabelle.session, buffer, thy_name)
+            for (text_area <- Isabelle.jedit_text_areas(buffer)) {
+              if (Document_View(text_area).isEmpty)
+                Document_View.init(model, text_area)
+            }
+          }
       }
     }
   }
@@ -239,25 +245,26 @@
   {
     Isabelle.swing_buffer_lock(buffer) {
       for (text_area <- Isabelle.jedit_text_areas(buffer)) {
-        if (Document_View(text_area).isDefined) Document_View.exit(text_area)
+        if (Document_View(text_area).isDefined)
+          Document_View.exit(text_area)
       }
-      if (Document_Model(buffer).isDefined) Document_Model.exit(buffer)
+      if (Document_Model(buffer).isDefined)
+        Document_Model.exit(buffer)
     }
   }
 
-  private val session_manager = Simple_Thread.actor("session_manager", daemon = true) {
-    var finished = false
-    while (!finished) {
-      receive {
-        case (Session.Startup, Session.Exit) =>
+  private val session_manager = actor {
+    loop {
+      react {
+        case (Session.Inactive, Session.Exit) =>
           val text = new scala.swing.TextArea(Isabelle.session.syslog())
           text.editable = false
           Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
-          finished = true
 
         case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer)
         case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer)
-        case (_, Session.Terminated) => finished = true
+
+        case _ =>
       }
     }
   }
@@ -268,15 +275,16 @@
   override def handleMessage(message: EBMessage)
   {
     message match {
-      case msg: ViewUpdate
-        if msg.getWhat == ViewUpdate.ACTIVATED =>
-        session_startup()
+      case msg: EditorStarted => start_session()
 
       case msg: BufferUpdate
-        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
-        Document_Model(msg.getBuffer) match {
-          case Some(model) => model.refresh()
-          case _ =>
+      if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+        val buffer = msg.getBuffer
+        Isabelle.swing_buffer_lock(buffer) {
+          Document_Model(buffer) match {
+            case None => // FIXME activate_buffer(buffer)
+            case Some(model) => model.refresh()
+          }
         }
 
       case msg: EditPaneUpdate =>
@@ -321,13 +329,12 @@
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()
     Isabelle.session = new Session(Isabelle.system)
-    Isabelle.session.phase_changed += session_manager._2
+    Isabelle.session.phase_changed += session_manager
   }
 
   override def stop()
   {
     Isabelle.session.stop()
-    session_manager._1.join
-    Isabelle.session.phase_changed -= session_manager._2
+    Isabelle.session.phase_changed -= session_manager
   }
 }