# HG changeset patch # User wenzelm # Date 1262216295 -3600 # Node ID a8ba6cde13e974d8250a2c56139f3d91a2ba5400 # Parent 86cb7f8e5a0d209730e174554c938f7759b19ba7 basic setup for synchronous / modal (!) prover startup; diff -r 86cb7f8e5a0d -r a8ba6cde13e9 src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 86cb7f8e5a0d -r a8ba6cde13e9 src/Tools/jEdit/src/jedit/plugin.scala --- 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 = diff -r 86cb7f8e5a0d -r a8ba6cde13e9 src/Tools/jEdit/src/proofdocument/session.scala --- 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 }