basic setup for synchronous / modal (!) prover startup;

--- a/src/Tools/jEdit/plugin/Isabelle.props	Wed Dec 30 21:57:29 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Thu Dec 31 00:38:15 2009 +0100
@@ -26,6 +26,7 @@
 options.isabelle.logic.title=Logic
 options.isabelle.font-size.title=Font Size
 options.isabelle.font-size=14
+options.isabelle.startup-timeout=10000
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 30 21:57:29 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 31 00:38:15 2009 +0100
@@ -21,6 +21,7 @@
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+import org.gjt.sp.jedit.gui.EnhancedDialog
 
 
 object Isabelle
@@ -97,14 +98,34 @@
     jedit_text_areas().filter(_.getBuffer == buffer)
 
 
+  /* manage prover */
+
+  private def prover_started(view: View): Boolean =
+  {
+    val timeout = Int_Property("startup-timeout") max 1000
+    session.start(timeout, Isabelle.isabelle_args()) match {
+      case Some(err) =>
+        // FIXME proper dialog
+        val dialog = new EnhancedDialog(view, "Failed to start prover:\n" + err, true) {
+          def ok { dispose }
+          def cancel { dispose }
+        }
+        dialog.setVisible(true)
+        false
+      case None => true
+    }
+  }
+
+
   /* activation */
 
-  def activate_buffer(buffer: Buffer)
+  def activate_buffer(view: View, buffer: Buffer)
   {
-    session.start(Isabelle.isabelle_args())
-    val model = Document_Model.init(session, buffer)
-    for (text_area <- jedit_text_areas(buffer))
-      Document_View.init(model, text_area)
+    if (prover_started(view)) {
+      val model = Document_Model.init(session, buffer)
+      for (text_area <- jedit_text_areas(buffer))
+        Document_View.init(model, text_area)
+    }
   }
 
   def deactivate_buffer(buffer: Buffer)
@@ -120,7 +141,7 @@
   {
     val buffer = view.getBuffer
     if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
-    else activate_buffer(buffer)
+    else activate_buffer(view, buffer)
   }
 
   def is_active(view: View): Boolean =

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 21:57:29 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Thu Dec 31 00:38:15 2009 +0100
@@ -7,6 +7,7 @@
 package isabelle.proofdocument
 
 
+import scala.actors.TIMEOUT
 import scala.actors.Actor._
 
 
@@ -64,14 +65,13 @@
   /** main actor **/
 
   private case class Register(entity: Session.Entity)
-  private case class Start(args: List[String])
+  private case class Start(timeout: Int, args: List[String])
   private case object Stop
   private case class Begin_Document(path: String)
 
   private val session_actor = actor {
 
     var prover: Isabelle_Process with Isar_Document = null
-    var prover_ready = false
 
     def register(entity: Session.Entity) { entities += (entity.id -> entity) }
 
@@ -124,10 +124,7 @@
             case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
               syntax += name
 
-            // process ready (after initialization)
-            case XML.Elem(Markup.READY, _, _) => prover_ready = true
-
-          case _ =>
+            case _ =>
           }
         }
       }
@@ -135,29 +132,73 @@
         prover = null
     }
 
-    val xml_cache = new XML.Cache(131071)
+
+    /* prover startup */
+
+    def startup_error(): String =
+    {
+      val buf = new StringBuilder
+      while (
+        receiveWithin(0) {
+          case result: Isabelle_Process.Result =>
+            if (result.is_raw) {
+              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.kind == Isabelle_Process.Kind.INIT =>
+          while (receive {
+            case result: Isabelle_Process.Result =>
+              handle_result(result); !result.is_ready
+            }) {}
+          None
+
+        case result: Isabelle_Process.Result
+          if result.kind == Isabelle_Process.Kind.EXIT =>
+          Some(startup_error())
+
+        case TIMEOUT =>  // FIXME clarify
+          prover.kill; Some(startup_error())
+      }
+    }
 
 
     /* main loop */
 
+    val xml_cache = new XML.Cache(131071)
+
     loop {
       react {
         case Register(entity: Session.Entity) =>
           register(entity)
           reply(())
 
-        case Start(args) =>
+        case Start(timeout, args) =>
           if (prover == null) {
             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
-            reply(())
+            val origin = sender
+            val opt_err = prover_startup(timeout)
+            if (opt_err.isDefined) prover = null
+            origin ! opt_err
+          }
+          else reply(None)
+
+        case Stop =>  // FIXME clarify; synchronous
+          if (prover != null) {
+            prover.kill
+            prover = null
           }
 
-        case Stop =>  // FIXME clarify
-          if (prover != null)
-            prover.kill
-          prover_ready = false
-
-        case Begin_Document(path: String) if prover_ready =>
+        case Begin_Document(path: String) if prover != null =>
           val id = create_id()
           val doc = Proof_Document.empty(id)
           register(doc)
@@ -165,13 +206,13 @@
           prover.begin_document(id, path)
           reply(doc)
 
-        case change: Change if prover_ready =>
+        case change: Change if prover != null =>
           handle_change(change)
 
         case result: Isabelle_Process.Result =>
           handle_result(result.cache(xml_cache))
 
-        case bad if prover_ready =>
+        case bad if prover != null =>
           System.err.println("session_actor: ignoring bad message " + bad)
       }
     }
@@ -182,7 +223,9 @@
 
   def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
 
-  def start(args: List[String]) { session_actor !? Start(args) }
+  def start(timeout: Int, args: List[String]): Option[String] =
+    (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
+
   def stop() { session_actor ! Stop }
   def input(change: Change) { session_actor ! change }