# HG changeset patch # User wenzelm # Date 1285260266 -7200 # Node ID 44181423183af261f4d2806d41553b2bceb98977 # Parent 08eb2730a8a19789ebb3835383c87b6c0017b4f9 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; diff -r 08eb2730a8a1 -r 44181423183a src/Pure/System/isabelle_process.scala --- 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 diff -r 08eb2730a8a1 -r 44181423183a src/Pure/System/session.scala --- 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 } diff -r 08eb2730a8a1 -r 44181423183a src/Pure/Thy/thy_header.scala --- 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 } } diff -r 08eb2730a8a1 -r 44181423183a src/Tools/jEdit/dist-template/properties/jedit.props --- 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 diff -r 08eb2730a8a1 -r 44181423183a src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 08eb2730a8a1 -r 44181423183a src/Tools/jEdit/plugin/actions.xml --- 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 @@ - - - isabelle.jedit.Isabelle.switch_active(view); - - - return isabelle.jedit.Isabelle.is_active(view); - - wm.addDockableWindow("isabelle-session"); diff -r 08eb2730a8a1 -r 44181423183a src/Tools/jEdit/src/jedit/plugin.scala --- 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 } }