1.1 --- a/src/Pure/System/isabelle_process.scala Thu Sep 23 16:48:48 2010 +0200
1.2 +++ b/src/Pure/System/isabelle_process.scala Thu Sep 23 18:44:26 2010 +0200
1.3 @@ -13,7 +13,6 @@
1.4
1.5 import scala.actors.Actor
1.6 import Actor._
1.7 -import scala.collection.mutable
1.8
1.9
1.10 object Isabelle_Process
2.1 --- a/src/Pure/System/session.scala Thu Sep 23 16:48:48 2010 +0200
2.2 +++ b/src/Pure/System/session.scala Thu Sep 23 18:44:26 2010 +0200
2.3 @@ -21,6 +21,14 @@
2.4 case object Perspective
2.5 case object Assignment
2.6 case class Commands_Changed(set: Set[Command])
2.7 +
2.8 + sealed abstract class Phase
2.9 + case object Inactive extends Phase
2.10 + case object Startup extends Phase
2.11 + case object Exit extends Phase
2.12 + case object Ready extends Phase
2.13 + case object Shutdown extends Phase
2.14 + case object Terminated extends Phase
2.15 }
2.16
2.17
2.18 @@ -40,6 +48,7 @@
2.19
2.20 /* pervasive event buses */
2.21
2.22 + val phase_changed = new Event_Bus[(Session.Phase, Session.Phase)]
2.23 val global_settings = new Event_Bus[Session.Global_Settings.type]
2.24 val raw_messages = new Event_Bus[Isabelle_Process.Result]
2.25 val commands_changed = new Event_Bus[Session.Commands_Changed]
2.26 @@ -98,7 +107,7 @@
2.27 receiveWithin(flush_timeout) {
2.28 case command: Command => changed += command; invoke()
2.29 case TIMEOUT => flush()
2.30 - case Stop => finished = true
2.31 + case Stop => finished = true; reply(())
2.32 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
2.33 }
2.34 }
2.35 @@ -115,12 +124,21 @@
2.36 @volatile private var reverse_syslog = List[XML.Elem]()
2.37 def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
2.38
2.39 + @volatile private var _phase: Session.Phase = Session.Inactive
2.40 + def phase = _phase
2.41 + def phase_=(new_phase: Session.Phase)
2.42 + {
2.43 + val old_phase = _phase
2.44 + _phase = new_phase
2.45 + phase_changed.event(old_phase, new_phase)
2.46 + }
2.47 +
2.48 private val global_state = new Volatile(Document.State.init)
2.49 def current_state(): Document.State = global_state.peek()
2.50
2.51 private case object Interrupt_Prover
2.52 private case class Edit_Version(edits: List[Document.Node_Text_Edit])
2.53 - private case class Started(timeout: Int, args: List[String])
2.54 + private case class Start(timeout: Int, args: List[String])
2.55
2.56 private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
2.57 {
2.58 @@ -190,8 +208,11 @@
2.59 }
2.60 catch { case _: Document.State.Fail => bad_result(result) }
2.61 case _ =>
2.62 - if (result.is_exit) prover = null // FIXME ??
2.63 - else if (result.is_syslog) reverse_syslog ::= result.message
2.64 + if (result.is_syslog) {
2.65 + reverse_syslog ::= result.message
2.66 + if (result.is_ready) phase = Session.Ready
2.67 + else if (result.is_exit) phase = Session.Exit
2.68 + }
2.69 else if (result.is_stdout) { }
2.70 else if (result.is_status) {
2.71 result.body match {
2.72 @@ -213,46 +234,7 @@
2.73 //}}}
2.74
2.75
2.76 - /* prover startup */
2.77 -
2.78 - def startup_error(): String =
2.79 - {
2.80 - val buf = new StringBuilder
2.81 - while (
2.82 - receiveWithin(0) {
2.83 - case result: Isabelle_Process.Result =>
2.84 - if (result.is_system) {
2.85 - for (text <- XML.content(result.message))
2.86 - buf.append(text)
2.87 - }
2.88 - true
2.89 - case TIMEOUT => false
2.90 - }) {}
2.91 - buf.toString
2.92 - }
2.93 -
2.94 - def prover_startup(timeout: Int): Option[String] =
2.95 - {
2.96 - receiveWithin(timeout) {
2.97 - case result: Isabelle_Process.Result if result.is_init =>
2.98 - handle_result(result)
2.99 - while (receive {
2.100 - case result: Isabelle_Process.Result =>
2.101 - handle_result(result); !result.is_ready
2.102 - }) {}
2.103 - None
2.104 -
2.105 - case result: Isabelle_Process.Result if result.is_exit =>
2.106 - handle_result(result)
2.107 - Some(startup_error())
2.108 -
2.109 - case TIMEOUT => // FIXME clarify
2.110 - prover.terminate; Some(startup_error())
2.111 - }
2.112 - }
2.113 -
2.114 -
2.115 - /* main loop */ // FIXME proper shutdown
2.116 + /* main loop */
2.117
2.118 var finished = false
2.119 while (!finished) {
2.120 @@ -260,7 +242,7 @@
2.121 case Interrupt_Prover =>
2.122 if (prover != null) prover.interrupt
2.123
2.124 - case Edit_Version(edits) =>
2.125 + case Edit_Version(edits) if prover != null =>
2.126 val previous = global_state.peek().history.tip.current
2.127 val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
2.128 val change = global_state.change_yield(_.extend_history(previous, edits, result))
2.129 @@ -272,30 +254,21 @@
2.130
2.131 reply(())
2.132
2.133 - case change: Document.Change if prover != null =>
2.134 - handle_change(change)
2.135 + case change: Document.Change if prover != null => handle_change(change)
2.136
2.137 - case result: Isabelle_Process.Result =>
2.138 - handle_result(result)
2.139 + case result: Isabelle_Process.Result => handle_result(result)
2.140
2.141 - case Started(timeout, args) =>
2.142 - if (prover == null) {
2.143 - prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
2.144 - val origin = sender
2.145 - val opt_err = prover_startup(timeout + 500)
2.146 - if (opt_err.isDefined) prover = null
2.147 - origin ! opt_err
2.148 - }
2.149 - else reply(None)
2.150 + case Start(timeout, args) if prover == null =>
2.151 + phase = Session.Startup
2.152 + prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
2.153
2.154 - case Stop => // FIXME synchronous!?
2.155 - if (prover != null) {
2.156 - global_state.change(_ => Document.State.init)
2.157 - prover.terminate
2.158 - prover = null
2.159 - }
2.160 -
2.161 - case TIMEOUT => // FIXME clarify
2.162 + case Stop if phase == Session.Ready =>
2.163 + global_state.change(_ => Document.State.init) // FIXME event bus!?
2.164 + phase = Session.Shutdown
2.165 + prover.terminate
2.166 + phase = Session.Terminated
2.167 + finished = true
2.168 + reply(())
2.169
2.170 case bad if prover != null =>
2.171 System.err.println("session_actor: ignoring bad message " + bad)
2.172 @@ -307,10 +280,9 @@
2.173
2.174 /** main methods **/
2.175
2.176 - def started(timeout: Int, args: List[String]): Option[String] =
2.177 - (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
2.178 + def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
2.179
2.180 - def stop() { command_change_buffer ! Stop; session_actor ! Stop }
2.181 + def stop() { command_change_buffer !? Stop; session_actor !? Stop }
2.182
2.183 def interrupt() { session_actor ! Interrupt_Prover }
2.184
3.1 --- a/src/Pure/Thy/thy_header.scala Thu Sep 23 16:48:48 2010 +0200
3.2 +++ b/src/Pure/Thy/thy_header.scala Thu Sep 23 18:44:26 2010 +0200
3.3 @@ -32,11 +32,11 @@
3.4 val Thy_Path1 = new Regex("([^/]*)\\.thy")
3.5 val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
3.6
3.7 - def split_thy_path(path: String): (String, String) =
3.8 + def split_thy_path(path: String): Option[(String, String)] =
3.9 path match {
3.10 - case Thy_Path1(name) => ("", name)
3.11 - case Thy_Path2(dir, name) => (dir, name)
3.12 - case _ => error("Bad theory file specification: " + path)
3.13 + case Thy_Path1(name) => Some(("", name))
3.14 + case Thy_Path2(dir, name) => Some((dir, name))
3.15 + case _ => None
3.16 }
3.17 }
3.18
4.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props Thu Sep 23 16:48:48 2010 +0200
4.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Thu Sep 23 18:44:26 2010 +0200
4.3 @@ -183,7 +183,6 @@
4.4 isabelle-output.dock-position=bottom
4.5 isabelle-raw-output.dock-position=bottom
4.6 isabelle-session.dock-position=bottom
4.7 -isabelle.activate.shortcut=CS+ENTER
4.8 line-end.shortcut=END
4.9 line-home.shortcut=HOME
4.10 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
5.1 --- a/src/Tools/jEdit/plugin/Isabelle.props Thu Sep 23 16:48:48 2010 +0200
5.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props Thu Sep 23 18:44:26 2010 +0200
5.3 @@ -35,8 +35,7 @@
5.4
5.5 #menu actions
5.6 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
5.7 -plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
5.8 -isabelle.activate.label=Activate current buffer
5.9 +plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
5.10 isabelle.session-panel.label=Prover Session panel
5.11 isabelle.output-panel.label=Output panel
5.12 isabelle.raw-output-panel.label=Raw Output panel
6.1 --- a/src/Tools/jEdit/plugin/actions.xml Thu Sep 23 16:48:48 2010 +0200
6.2 +++ b/src/Tools/jEdit/plugin/actions.xml Thu Sep 23 18:44:26 2010 +0200
6.3 @@ -2,14 +2,6 @@
6.4 <!DOCTYPE ACTIONS SYSTEM "actions.dtd">
6.5
6.6 <ACTIONS>
6.7 - <ACTION NAME="isabelle.activate">
6.8 - <CODE>
6.9 - isabelle.jedit.Isabelle.switch_active(view);
6.10 - </CODE>
6.11 - <IS_SELECTED>
6.12 - return isabelle.jedit.Isabelle.is_active(view);
6.13 - </IS_SELECTED>
6.14 - </ACTION>
6.15 <ACTION NAME="isabelle.session-panel">
6.16 <CODE>
6.17 wm.addDockableWindow("isabelle-session");
7.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala Thu Sep 23 16:48:48 2010 +0200
7.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Thu Sep 23 18:44:26 2010 +0200
7.3 @@ -19,11 +19,14 @@
7.4 Buffer, EditPane, ServiceManager, View}
7.5 import org.gjt.sp.jedit.buffer.JEditBuffer
7.6 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
7.7 -import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
7.8 +import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged, ViewUpdate}
7.9 import org.gjt.sp.jedit.gui.DockableWindowManager
7.10
7.11 import org.gjt.sp.util.Log
7.12
7.13 +import scala.actors.Actor
7.14 +import Actor._
7.15 +
7.16
7.17 object Isabelle
7.18 {
7.19 @@ -115,7 +118,7 @@
7.20 {
7.21 val icon = GUIUtilities.loadIcon(name)
7.22 if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
7.23 - Log.log(Log.ERROR, icon, "Bad icon: " + name);
7.24 + Log.log(Log.ERROR, icon, "Bad icon: " + name)
7.25 icon
7.26 }
7.27
7.28 @@ -200,77 +203,76 @@
7.29 }
7.30 component
7.31 }
7.32 +}
7.33
7.34 - def isabelle_args(): List[String] =
7.35 +
7.36 +class Plugin extends EBPlugin
7.37 +{
7.38 + /* session management */
7.39 +
7.40 + private def session_startup()
7.41 {
7.42 - val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
7.43 + val timeout = Isabelle.Int_Property("startup-timeout") max 1000
7.44 + val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
7.45 val logic = {
7.46 - val logic = Property("logic")
7.47 + val logic = Isabelle.Property("logic")
7.48 if (logic != null && logic != "") logic
7.49 - else default_logic()
7.50 + else Isabelle.default_logic()
7.51 }
7.52 - modes ++ List(logic)
7.53 + Isabelle.session.start(timeout, modes ::: List(logic))
7.54 }
7.55
7.56 -
7.57 - /* manage prover */ // FIXME async!?
7.58 -
7.59 - private def prover_started(view: View): Boolean =
7.60 + private def activate_buffer(buffer: Buffer)
7.61 {
7.62 - val timeout = Int_Property("startup-timeout") max 1000
7.63 - session.started(timeout, Isabelle.isabelle_args()) match {
7.64 - case Some(err) =>
7.65 - val text = new scala.swing.TextArea(err)
7.66 - text.editable = false
7.67 - Library.error_dialog(view, null, "Failed to start Isabelle process", text)
7.68 - false
7.69 - case None => true
7.70 + Isabelle.swing_buffer_lock(buffer) {
7.71 + Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
7.72 + case None =>
7.73 + case Some((_, thy_name)) =>
7.74 + val model = Document_Model.init(Isabelle.session, buffer, thy_name)
7.75 + for (text_area <- Isabelle.jedit_text_areas(buffer))
7.76 + Document_View.init(model, text_area)
7.77 + }
7.78 }
7.79 }
7.80
7.81 -
7.82 - /* activation */
7.83 -
7.84 - def activate_buffer(view: View, buffer: Buffer)
7.85 + private def deactivate_buffer(buffer: Buffer)
7.86 {
7.87 - if (prover_started(view)) {
7.88 - // FIXME proper error handling
7.89 - val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
7.90 -
7.91 - val model = Document_Model.init(session, buffer, thy_name)
7.92 - for (text_area <- jedit_text_areas(buffer))
7.93 - Document_View.init(model, text_area)
7.94 + Isabelle.swing_buffer_lock(buffer) {
7.95 + for (text_area <- Isabelle.jedit_text_areas(buffer)) {
7.96 + if (Document_View(text_area).isDefined) Document_View.exit(text_area)
7.97 + }
7.98 + if (Document_Model(buffer).isDefined) Document_Model.exit(buffer)
7.99 }
7.100 }
7.101
7.102 - def deactivate_buffer(buffer: Buffer)
7.103 - {
7.104 - session.stop() // FIXME not yet
7.105 + private val session_manager = Simple_Thread.actor("session_manager", daemon = true) {
7.106 + var finished = false
7.107 + while (!finished) {
7.108 + receive {
7.109 + case (Session.Startup, Session.Exit) =>
7.110 + val text = new scala.swing.TextArea(Isabelle.session.syslog())
7.111 + text.editable = false
7.112 + // FIXME proper view!?
7.113 + Library.error_dialog(null, null, "Failed to start Isabelle process", text)
7.114 + finished = true
7.115
7.116 - for (text_area <- jedit_text_areas(buffer))
7.117 - Document_View.exit(text_area)
7.118 - Document_Model.exit(buffer)
7.119 + case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer)
7.120 + case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer)
7.121 + case (_, Session.Terminated) => finished = true
7.122 + }
7.123 + }
7.124 }
7.125
7.126 - def switch_active(view: View) =
7.127 - {
7.128 - val buffer = view.getBuffer
7.129 - if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
7.130 - else activate_buffer(view, buffer)
7.131 - }
7.132
7.133 - def is_active(view: View): Boolean =
7.134 - Document_Model(view.getBuffer).isDefined
7.135 -}
7.136 -
7.137 -
7.138 -class Plugin extends EBPlugin
7.139 -{
7.140 /* main plugin plumbing */
7.141
7.142 override def handleMessage(message: EBMessage)
7.143 {
7.144 message match {
7.145 + case msg: ViewUpdate
7.146 + if msg.getWhat == ViewUpdate.ACTIVATED =>
7.147 + session_startup()
7.148 +
7.149 case msg: BufferUpdate
7.150 if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
7.151 Document_Model(msg.getBuffer) match {
7.152 @@ -304,12 +306,10 @@
7.153
7.154 case msg: PropertiesChanged =>
7.155 Swing_Thread.now {
7.156 + Isabelle.setup_tooltips()
7.157 for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
7.158 Document_View(text_area).get.extend_styles()
7.159 -
7.160 - Isabelle.setup_tooltips()
7.161 }
7.162 -
7.163 Isabelle.session.global_settings.event(Session.Global_Settings)
7.164
7.165 case _ =>
7.166 @@ -318,14 +318,17 @@
7.167
7.168 override def start()
7.169 {
7.170 + Isabelle.setup_tooltips()
7.171 Isabelle.system = new Isabelle_System
7.172 Isabelle.system.install_fonts()
7.173 Isabelle.session = new Session(Isabelle.system)
7.174 - Isabelle.setup_tooltips()
7.175 + Isabelle.session.phase_changed += session_manager._2
7.176 }
7.177
7.178 override def stop()
7.179 {
7.180 Isabelle.session.stop()
7.181 + session_manager._1.join
7.182 + Isabelle.session.phase_changed -= session_manager._2
7.183 }
7.184 }