explicit Session.Phase indication with associated event bus;
asynchronous Session.start();
synchronous Session.stop();
added Plugin.session_manager on top of basic Session;
eliminated separate isabelle.activate action;
misc tuning;

--- a/src/Pure/System/isabelle_process.scala	Thu Sep 23 16:48:48 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Sep 23 18:44:26 2010 +0200
@@ -13,7 +13,6 @@
 
 import scala.actors.Actor
 import Actor._
-import scala.collection.mutable
 
 
 object Isabelle_Process

--- a/src/Pure/System/session.scala	Thu Sep 23 16:48:48 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Sep 23 18:44:26 2010 +0200
@@ -21,6 +21,14 @@
   case object Perspective
   case object Assignment
   case class Commands_Changed(set: Set[Command])
+
+  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
 }
 
 
@@ -40,6 +48,7 @@
 
   /* pervasive event buses */
 
+  val phase_changed = new Event_Bus[(Session.Phase, 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]
@@ -98,7 +107,7 @@
       receiveWithin(flush_timeout) {
         case command: Command => changed += command; invoke()
         case TIMEOUT => flush()
-        case Stop => finished = true
+        case Stop => finished = true; reply(())
         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
       }
     }
@@ -115,12 +124,21 @@
   @volatile private var reverse_syslog = List[XML.Elem]()
   def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
 
+  @volatile private var _phase: Session.Phase = Session.Inactive
+  def phase = _phase
+  def phase_=(new_phase: Session.Phase)
+  {
+    val old_phase = _phase
+    _phase = new_phase
+    phase_changed.event(old_phase, new_phase)
+  }
+
   private val global_state = new Volatile(Document.State.init)
   def current_state(): Document.State = global_state.peek()
 
   private case object Interrupt_Prover
   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
-  private case class Started(timeout: Int, args: List[String])
+  private case class Start(timeout: Int, args: List[String])
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
@@ -190,8 +208,11 @@
           }
           catch { case _: Document.State.Fail => bad_result(result) }
         case _ =>
-          if (result.is_exit) prover = null  // FIXME ??
-          else if (result.is_syslog) reverse_syslog ::= result.message
+          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_stdout) { }
           else if (result.is_status) {
             result.body match {
@@ -213,46 +234,7 @@
     //}}}
 
 
-    /* prover startup */
-
-    def startup_error(): String =
-    {
-      val buf = new StringBuilder
-      while (
-        receiveWithin(0) {
-          case result: Isabelle_Process.Result =>
-            if (result.is_system) {
-              for (text <- XML.content(result.message))
-                buf.append(text)
-            }
-            true
-          case TIMEOUT => false
-        }) {}
-      buf.toString
-    }
-
-    def prover_startup(timeout: Int): Option[String] =
-    {
-      receiveWithin(timeout) {
-        case result: Isabelle_Process.Result if result.is_init =>
-          handle_result(result)
-          while (receive {
-            case result: Isabelle_Process.Result =>
-              handle_result(result); !result.is_ready
-            }) {}
-          None
-
-        case result: Isabelle_Process.Result if result.is_exit =>
-          handle_result(result)
-          Some(startup_error())
-
-        case TIMEOUT =>  // FIXME clarify
-          prover.terminate; Some(startup_error())
-      }
-    }
-
-
-    /* main loop */  // FIXME proper shutdown
+    /* main loop */
 
     var finished = false
     while (!finished) {
@@ -260,7 +242,7 @@
         case Interrupt_Prover =>
           if (prover != null) prover.interrupt
 
-        case Edit_Version(edits) =>
+        case Edit_Version(edits) if prover != null =>
           val previous = global_state.peek().history.tip.current
           val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
           val change = global_state.change_yield(_.extend_history(previous, edits, result))
@@ -272,30 +254,21 @@
 
           reply(())
 
-        case change: Document.Change if prover != null =>
-          handle_change(change)
+        case change: Document.Change if prover != null => handle_change(change)
+
+        case result: Isabelle_Process.Result => handle_result(result)
 
-        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 Started(timeout, args) =>
-          if (prover == null) {
-            prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
-            val origin = sender
-            val opt_err = prover_startup(timeout + 500)
-            if (opt_err.isDefined) prover = null
-            origin ! opt_err
-          }
-          else reply(None)
-
-        case Stop => // FIXME synchronous!?
-          if (prover != null) {
-            global_state.change(_ => Document.State.init)
-            prover.terminate
-            prover = null
-          }
-
-        case TIMEOUT =>  // FIXME clarify
+        case Stop if phase == Session.Ready =>
+          global_state.change(_ => Document.State.init)  // FIXME event bus!?
+          phase = Session.Shutdown
+          prover.terminate
+          phase = Session.Terminated
+          finished = true
+          reply(())
 
         case bad if prover != null =>
           System.err.println("session_actor: ignoring bad message " + bad)
@@ -307,10 +280,9 @@
 
   /** main methods **/
 
-  def started(timeout: Int, args: List[String]): Option[String] =
-    (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
+  def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
 
-  def stop() { command_change_buffer ! Stop; session_actor ! Stop }
+  def stop() { command_change_buffer !? Stop; session_actor !? Stop }
 
   def interrupt() { session_actor ! Interrupt_Prover }
 

--- a/src/Pure/Thy/thy_header.scala	Thu Sep 23 16:48:48 2010 +0200
+++ b/src/Pure/Thy/thy_header.scala	Thu Sep 23 18:44:26 2010 +0200
@@ -32,11 +32,11 @@
   val Thy_Path1 = new Regex("([^/]*)\\.thy")
   val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
 
-  def split_thy_path(path: String): (String, String) =
+  def split_thy_path(path: String): Option[(String, String)] =
     path match {
-      case Thy_Path1(name) => ("", name)
-      case Thy_Path2(dir, name) => (dir, name)
-      case _ => error("Bad theory file specification: " + path)
+      case Thy_Path1(name) => Some(("", name))
+      case Thy_Path2(dir, name) => Some((dir, name))
+      case _ => None
     }
 }
 

--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Thu Sep 23 16:48:48 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Thu Sep 23 18:44:26 2010 +0200
@@ -183,7 +183,6 @@
 isabelle-output.dock-position=bottom
 isabelle-raw-output.dock-position=bottom
 isabelle-session.dock-position=bottom
-isabelle.activate.shortcut=CS+ENTER
 line-end.shortcut=END
 line-home.shortcut=HOME
 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel

--- a/src/Tools/jEdit/plugin/Isabelle.props	Thu Sep 23 16:48:48 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Thu Sep 23 18:44:26 2010 +0200
@@ -35,8 +35,7 @@
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
-isabelle.activate.label=Activate current buffer
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
 isabelle.session-panel.label=Prover Session panel
 isabelle.output-panel.label=Output panel
 isabelle.raw-output-panel.label=Raw Output panel

--- a/src/Tools/jEdit/plugin/actions.xml	Thu Sep 23 16:48:48 2010 +0200
+++ b/src/Tools/jEdit/plugin/actions.xml	Thu Sep 23 18:44:26 2010 +0200
@@ -2,14 +2,6 @@
 <!DOCTYPE ACTIONS SYSTEM "actions.dtd">
 
 <ACTIONS>
-  <ACTION NAME="isabelle.activate">
-		<CODE>
-			isabelle.jedit.Isabelle.switch_active(view);
-		</CODE>
-		<IS_SELECTED>
-			return isabelle.jedit.Isabelle.is_active(view);
-		</IS_SELECTED>
-	</ACTION>
 	<ACTION NAME="isabelle.session-panel">
 		<CODE>
 			wm.addDockableWindow("isabelle-session");

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 16:48:48 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 18:44:26 2010 +0200
@@ -19,11 +19,14 @@
   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}
+import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged, ViewUpdate}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 import org.gjt.sp.util.Log
 
+import scala.actors.Actor
+import Actor._
+
 
 object Isabelle
 {
@@ -115,7 +118,7 @@
   {
     val icon = GUIUtilities.loadIcon(name)
     if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
-      Log.log(Log.ERROR, icon, "Bad icon: " + name);
+      Log.log(Log.ERROR, icon, "Bad icon: " + name)
     icon
   }
 
@@ -200,77 +203,76 @@
     }
     component
   }
-
-  def isabelle_args(): List[String] =
-  {
-    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
-    val logic = {
-      val logic = Property("logic")
-      if (logic != null && logic != "") logic
-      else default_logic()
-    }
-    modes ++ List(logic)
-  }
-
-
-  /* manage prover */  // FIXME async!?
-
-  private def prover_started(view: View): Boolean =
-  {
-    val timeout = Int_Property("startup-timeout") max 1000
-    session.started(timeout, Isabelle.isabelle_args()) match {
-      case Some(err) =>
-        val text = new scala.swing.TextArea(err)
-        text.editable = false
-        Library.error_dialog(view, null, "Failed to start Isabelle process", text)
-        false
-      case None => true
-    }
-  }
-
-
-  /* activation */
-
-  def activate_buffer(view: View, buffer: Buffer)
-  {
-    if (prover_started(view)) {
-      // FIXME proper error handling
-      val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
-
-      val model = Document_Model.init(session, buffer, thy_name)
-      for (text_area <- jedit_text_areas(buffer))
-        Document_View.init(model, text_area)
-    }
-  }
-
-  def deactivate_buffer(buffer: Buffer)
-  {
-    session.stop()  // FIXME not yet
-
-    for (text_area <- jedit_text_areas(buffer))
-      Document_View.exit(text_area)
-    Document_Model.exit(buffer)
-  }
-
-  def switch_active(view: View) =
-  {
-    val buffer = view.getBuffer
-    if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
-    else activate_buffer(view, buffer)
-  }
-
-  def is_active(view: View): Boolean =
-    Document_Model(view.getBuffer).isDefined
 }
 
 
 class Plugin extends EBPlugin
 {
+  /* session management */
+
+  private def session_startup()
+  {
+    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 activate_buffer(buffer: Buffer)
+  {
+    Isabelle.swing_buffer_lock(buffer) {
+      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)
+      }
+    }
+  }
+
+  private def deactivate_buffer(buffer: Buffer)
+  {
+    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_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) =>
+          val text = new scala.swing.TextArea(Isabelle.session.syslog())
+          text.editable = false
+          // FIXME proper view!?
+          Library.error_dialog(null, null, "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
+      }
+    }
+  }
+
+
   /* main plugin plumbing */
 
   override def handleMessage(message: EBMessage)
   {
     message match {
+      case msg: ViewUpdate
+        if msg.getWhat == ViewUpdate.ACTIVATED =>
+        session_startup()
+
       case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
         Document_Model(msg.getBuffer) match {
@@ -304,12 +306,10 @@
 
       case msg: PropertiesChanged =>
         Swing_Thread.now {
+          Isabelle.setup_tooltips()
           for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
             Document_View(text_area).get.extend_styles()
-
-          Isabelle.setup_tooltips()
         }
-
         Isabelle.session.global_settings.event(Session.Global_Settings)
 
       case _ =>
@@ -318,14 +318,17 @@
 
   override def start()
   {
+    Isabelle.setup_tooltips()
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()
     Isabelle.session = new Session(Isabelle.system)
-    Isabelle.setup_tooltips()
+    Isabelle.session.phase_changed += session_manager._2
   }
 
   override def stop()
   {
     Isabelle.session.stop()
+    session_manager._1.join
+    Isabelle.session.phase_changed -= session_manager._2
   }
 }