# HG changeset patch # User wenzelm # Date 1285334095 -7200 # Node ID 6814630157b9afa87aa046e602825f25e2107434 # Parent f75a01ee6c41dc12dc23fda965561de060ad26fc# Parent 2f9b6d2cf13d1666e0041db7eb106204e08fce0d merged diff -r f75a01ee6c41 -r 6814630157b9 Admin/polyml/build --- a/Admin/polyml/build Fri Sep 24 15:11:38 2010 +0200 +++ b/Admin/polyml/build Fri Sep 24 15:14:55 2010 +0200 @@ -77,6 +77,7 @@ { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \ make compiler && \ + make compiler && \ make install; } || fail "Build failed" ) diff -r f75a01ee6c41 -r 6814630157b9 lib/scripts/run-polyml --- a/lib/scripts/run-polyml Fri Sep 24 15:11:38 2010 +0200 +++ b/lib/scripts/run-polyml Fri Sep 24 15:14:55 2010 +0200 @@ -52,17 +52,18 @@ fi if [ -z "$OUTFILE" ]; then - COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' + COMMIT='fun commit () = false;' + MLEXIT="" else COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } + MLEXIT="commit();" fi ## run it! MLTEXT="$INIT $EXIT $COMMIT $MLTEXT" -MLEXIT="commit();" if [ -z "$TERMINATE" ]; then FEEDER_OPTS="" diff -r f75a01ee6c41 -r 6814630157b9 lib/scripts/run-smlnj --- a/lib/scripts/run-smlnj Fri Sep 24 15:11:38 2010 +0200 +++ b/lib/scripts/run-smlnj Fri Sep 24 15:14:55 2010 +0200 @@ -57,17 +57,18 @@ fi if [ -z "$OUTFILE" ]; then - COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' + COMMIT='fun commit () = false;' + MLEXIT="" else COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");" [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } + MLEXIT="commit();" fi ## run it! MLTEXT="$EXIT $COMMIT $MLTEXT" -MLEXIT="commit();" if [ -z "$TERMINATE" ]; then FEEDER_OPTS="" diff -r f75a01ee6c41 -r 6814630157b9 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Pure/PIDE/command.scala Fri Sep 24 15:14:55 2010 +0200 @@ -60,10 +60,14 @@ atts match { case Markup.Serial(i) => val result = XML.Elem(Markup(name, Position.purge(atts)), body) + val st0 = add_result(i, result) val st1 = - (add_result(i, result) /: Isar_Document.message_positions(command, message))( - (st, range) => st.add_markup(Text.Info(range, result))) - (st1 /: Isar_Document.message_reports(message))(_ accumulate _) + if (Isar_Document.is_tracing(message)) st0 + else + (st0 /: Isar_Document.message_positions(command, message))( + (st, range) => st.add_markup(Text.Info(range, result))) + val st2 = (st1 /: Isar_Document.message_reports(message))(_ accumulate _) + st2 case _ => System.err.println("Ignored message without serial number: " + message); this } } diff -r f75a01ee6c41 -r 6814630157b9 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Pure/PIDE/document.scala Fri Sep 24 15:14:55 2010 +0200 @@ -305,10 +305,18 @@ def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) def convert(range: Text.Range): Text.Range = - if (edits.isEmpty) range else range.map(convert(_)) + try { if (edits.isEmpty) range else range.map(convert(_)) } + catch { // FIXME tmp + case e: IllegalArgumentException => + System.err.println((true, range, edits)); throw(e) + } def revert(range: Text.Range): Text.Range = - if (edits.isEmpty) range else range.map(revert(_)) + try { if (edits.isEmpty) range else range.map(revert(_)) } + catch { // FIXME tmp + case e: IllegalArgumentException => + System.err.println((false, range, reverse_edits)); throw(e) + } def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A]) : Stream[Text.Info[Option[A]]] = diff -r f75a01ee6c41 -r 6814630157b9 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Pure/PIDE/isar_document.scala Fri Sep 24 15:14:55 2010 +0200 @@ -72,6 +72,19 @@ /* specific messages */ + def is_ready(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Markup.STATUS, _), + List(XML.Elem(Markup(Markup.READY, _), _))) => true + case _ => false + } + + def is_tracing(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Markup.TRACING, _), _) => true + case _ => false + } + def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WARNING, _), _) => true @@ -86,14 +99,16 @@ def is_state(msg: XML.Tree): Boolean = msg match { - case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true + case XML.Elem(Markup(Markup.WRITELN, _), + List(XML.Elem(Markup(Markup.STATE, _), _))) => true case _ => false } /* reported positions */ - private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) + private val include_pos = + Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) def message_positions(command: Command, message: XML.Elem): Set[Text.Range] = { @@ -116,9 +131,6 @@ trait Isar_Document extends Isabelle_Process { - import Isar_Document._ - - /* commands */ def define_command(id: Document.Command_ID, text: String): Unit = diff -r f75a01ee6c41 -r 6814630157b9 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Pure/System/isabelle_process.ML Fri Sep 24 15:14:55 2010 +0200 @@ -182,7 +182,7 @@ val (in_stream, out_stream) = setup_channels in_fifo out_fifo; val _ = init_message out_stream; val _ = Keyword.status (); - val _ = Output.status (Markup.markup Markup.ready "Prover ready"); + val _ = Output.status (Markup.markup Markup.ready "process ready"); in loop in_stream end)); end; diff -r f75a01ee6c41 -r 6814630157b9 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Pure/System/isabelle_process.scala Fri Sep 24 15:14:55 2010 +0200 @@ -13,7 +13,6 @@ import scala.actors.Actor import Actor._ -import scala.collection.mutable object Isabelle_Process @@ -44,11 +43,8 @@ def is_system = kind == Markup.SYSTEM def is_status = kind == Markup.STATUS def is_report = kind == Markup.REPORT - def is_ready = is_status && { - body match { - case List(XML.Elem(Markup(Markup.READY, _), _)) => true - case _ => false - }} + def is_ready = Isar_Document.is_ready(message) + def is_syslog = is_init || is_exit || is_system || is_ready override def toString: String = { @@ -77,21 +73,13 @@ actor { loop { react { case res => Console.println(res) } } }, args: _*) - /* system log */ - - private val system_results = new mutable.ListBuffer[String] + /* results */ private def system_result(text: String) { - synchronized { system_results += text } receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))) } - def syslog(): List[String] = synchronized { system_results.toList } - - - /* results */ - private val xml_cache = new XML.Cache(131071) private def put_result(kind: String, props: List[(String, String)], body: XML.Body) @@ -166,12 +154,12 @@ if (process_result.is_finished) finished = Some(false) else Thread.sleep(10) } - (finished.isEmpty || !finished.get, result.toString) + (finished.isEmpty || !finished.get, result.toString.trim) } system_result(startup_output) if (startup_failed) { - put_result(Markup.EXIT, "127") + put_result(Markup.EXIT, "Return code: 127") process.stdin.close Thread.sleep(300) terminate_process() @@ -188,10 +176,10 @@ val message = message_actor(message_stream) val rc = process_result.join - system_result("Isabelle process terminated") + system_result("process terminated") for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join system_result("process_manager terminated") - put_result(Markup.EXIT, rc.toString) + put_result(Markup.EXIT, "Return code: " + rc.toString) } rm_fifos() } diff -r f75a01ee6c41 -r 6814630157b9 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Pure/System/session.scala Fri Sep 24 15:14:55 2010 +0200 @@ -21,6 +21,12 @@ case object Perspective case object Assignment case class Commands_Changed(set: Set[Command]) + + sealed abstract class Phase + case object Inactive extends Phase + case object Exit extends Phase + case object Ready extends Phase + case object Shutdown extends Phase } @@ -40,6 +46,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 +105,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) } } @@ -112,12 +119,24 @@ @volatile private var syntax = new Outer_Syntax(system.symbols) def current_syntax(): Outer_Syntax = syntax + @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 + private 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) { @@ -187,7 +206,16 @@ } catch { case _: Document.State.Fail => bad_result(result) } case _ => - if (result.is_status) { + if (result.is_syslog) { + reverse_syslog ::= result.message + if (result.is_ready) phase = Session.Ready + else if (result.is_exit) { + phase = Session.Exit + phase = Session.Inactive + } + } + else if (result.is_stdout) { } + else if (result.is_status) { result.body match { case List(Isar_Document.Assign(id, edits)) => try { @@ -198,57 +226,16 @@ catch { case _: Document.State.Fail => bad_result(result) } case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) case List(Keyword.Keyword_Decl(name)) => syntax += name - case _ => if (!result.is_ready) bad_result(result) + case _ => bad_result(result) } } - else if (result.is_exit) prover = null // FIXME ?? - else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout)) - bad_result(result) + else bad_result(result) } } //}}} - /* 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) { @@ -256,7 +243,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)) @@ -268,30 +255,20 @@ 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 => + 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.Inactive + finished = true + reply(()) case bad if prover != null => System.err.println("session_actor: ignoring bad message " + bad) @@ -303,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 f75a01ee6c41 -r 6814630157b9 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Pure/Thy/thy_header.scala Fri Sep 24 15:14:55 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 f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/dist-template/properties/jedit.props --- a/src/Tools/jEdit/dist-template/properties/jedit.props Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Fri Sep 24 15:14:55 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 f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/plugin/Isabelle.props --- a/src/Tools/jEdit/plugin/Isabelle.props Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/plugin/Isabelle.props Fri Sep 24 15:14:55 2010 +0200 @@ -35,15 +35,14 @@ #menu actions plugin.isabelle.jedit.Plugin.menu.label=Isabelle -plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.session-panel isabelle.show-output isabelle.show-raw-output isabelle.show-protocol -isabelle.activate.label=Activate current buffer -isabelle.session-panel.label=Prover session panel -isabelle.show-output.label=Show Output -isabelle.show-raw-output.label=Show Raw Output -isabelle.show-protocol.label=Show Protocol +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 +isabelle.protocol-panel.label=Protocol panel #dockables -isabelle-session.title=Session +isabelle-session.title=Prover Session isabelle-output.title=Output isabelle-raw-output.title=Raw Output isabelle-protocol.title=Protocol diff -r f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/plugin/actions.xml --- a/src/Tools/jEdit/plugin/actions.xml Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/plugin/actions.xml Fri Sep 24 15:14:55 2010 +0200 @@ -2,30 +2,22 @@ - - - isabelle.jedit.Isabelle.switch_active(view); - - - return isabelle.jedit.Isabelle.is_active(view); - - wm.addDockableWindow("isabelle-session"); - + wm.addDockableWindow("isabelle-output"); - + wm.addDockableWindow("isabelle-raw-output"); - + wm.addDockableWindow("isabelle-protocol"); diff -r f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Fri Sep 24 15:14:55 2010 +0200 @@ -98,7 +98,7 @@ { Swing_Thread.require() apply(buffer) match { - case None => error("No document model for buffer: " + buffer) + case None => case Some(model) => model.deactivate() buffer.unsetProperty(key) diff -r f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Fri Sep 24 15:14:55 2010 +0200 @@ -52,7 +52,7 @@ { Swing_Thread.require() apply(text_area) match { - case None => error("No document view for text area: " + text_area) + case None => case Some(doc_view) => doc_view.deactivate() text_area.putClientProperty(key, null) diff -r f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri Sep 24 15:14:55 2010 +0200 @@ -66,24 +66,28 @@ override def complete(pane: EditPane, caret: Int): SideKickCompletion = { - // FIXME lock buffer (!?) val buffer = pane.getBuffer - - val line = buffer.getLineOfOffset(caret) - val start = buffer.getLineStartOffset(line) - val text = buffer.getSegment(start, caret - start) - - val completion = Isabelle.session.current_syntax().completion + Isabelle.swing_buffer_lock(buffer) { + Document_Model(buffer) match { + case None => null + case Some(model) => + val line = buffer.getLineOfOffset(caret) + val start = buffer.getLineStartOffset(line) + val text = buffer.getSegment(start, caret - start) - completion.complete(text) match { - case None => null - case Some((word, cs)) => - val ds = - (if (Isabelle_Encoding.is_active(buffer)) - cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _) - else cs).filter(_ != word) - if (ds.isEmpty) null - else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } + val completion = model.session.current_syntax().completion + completion.complete(text) match { + case None => null + case Some((word, cs)) => + val ds = + (if (Isabelle_Encoding.is_active(buffer)) + cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _) + else cs).filter(_ != word) + if (ds.isEmpty) null + else new SideKickCompletion( + pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } + } + } } } } diff -r f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Fri Sep 24 15:14:55 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.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} 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,116 +203,125 @@ } 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 start_session() + { + if (Isabelle.session.phase == Session.Inactive) { + 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 init_model(buffer: Buffer): Option[Document_Model] = + { + Document_Model(buffer) match { + case Some(model) => model.refresh; Some(model) + case None => + Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match { + case Some((_, thy_name)) => + Some(Document_Model.init(Isabelle.session, buffer, thy_name)) + case None => None + } + } + } + + private def activate_buffer(buffer: Buffer) + { + Isabelle.swing_buffer_lock(buffer) { + init_model(buffer) match { + case None => + case Some(model) => + for (text_area <- Isabelle.jedit_text_areas(buffer)) { + if (Document_View(text_area).map(_.model) != Some(model)) + Document_View.init(model, text_area) + } + } + } + } + + private def deactivate_buffer(buffer: Buffer) + { + Isabelle.swing_buffer_lock(buffer) { + Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit) + Document_Model.exit(buffer) + } + } + + private val session_manager = actor { + loop { + react { + case (Session.Inactive, Session.Exit) => + val text = new scala.swing.TextArea(Isabelle.session.syslog()) + text.editable = false + Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) + + case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer) + case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer) + + case _ => + } + } + } + + /* main plugin plumbing */ override def handleMessage(message: EBMessage) { message match { + case msg: EditorStarted => start_session() + case msg: BufferUpdate - if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => - Document_Model(msg.getBuffer) match { - case Some(model) => model.refresh() - case _ => - } + if Isabelle.session.phase == Session.Ready && + msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => + + val buffer = msg.getBuffer + if (buffer != null) activate_buffer(buffer) - case msg: EditPaneUpdate => + case msg: EditPaneUpdate + if Isabelle.session.phase == Session.Ready && + (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || + msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || + msg.getWhat == EditPaneUpdate.CREATED || + msg.getWhat == EditPaneUpdate.DESTROYED) => + val edit_pane = msg.getEditPane val buffer = edit_pane.getBuffer val text_area = edit_pane.getTextArea - def init_view() - { - Document_Model(buffer) match { - case Some(model) => Document_View.init(model, text_area) - case None => + if (buffer != null && text_area != null) { + Isabelle.swing_buffer_lock(buffer) { + msg.getWhat match { + case EditPaneUpdate.BUFFER_CHANGING | EditPaneUpdate.DESTROYED => + Document_View.exit(text_area) + case EditPaneUpdate.BUFFER_CHANGED | EditPaneUpdate.CREATED => + Document_Model(buffer) match { + case Some(model) => Document_View.init(model, text_area) + case None => + } + case _ => + } } } - def exit_view() - { - if (Document_View(text_area).isDefined) - Document_View.exit(text_area) - } - msg.getWhat match { - case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view() - case EditPaneUpdate.CREATED => init_view() - case EditPaneUpdate.DESTROYED => exit_view() - case _ => - } 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,16 +330,16 @@ override def start() { + Isabelle.setup_tooltips() Isabelle.system = new Isabelle_System Isabelle.system.install_fonts() - Isabelle.session = new Session(Isabelle.system) // FIXME dialog!? - - Isabelle.setup_tooltips() + Isabelle.session = new Session(Isabelle.system) + Isabelle.session.phase_changed += session_manager } - override def stop() // FIXME fragile + override def stop() { - Isabelle.session.stop() // FIXME dialog!? - Isabelle.session = null + Isabelle.session.stop() + Isabelle.session.phase_changed -= session_manager } } diff -r f75a01ee6c41 -r 6814630157b9 src/Tools/jEdit/src/jedit/session_dockable.scala --- a/src/Tools/jEdit/src/jedit/session_dockable.scala Fri Sep 24 15:11:38 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Fri Sep 24 15:14:55 2010 +0200 @@ -10,8 +10,9 @@ import isabelle._ import scala.actors.Actor._ -import scala.swing.{FlowPanel, Button, TextArea, ScrollPane, TabbedPane, Component} -import scala.swing.event.ButtonClicked +import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, + Component, Swing} +import scala.swing.event.{ButtonClicked, SelectionChanged} import java.awt.BorderLayout @@ -25,12 +26,23 @@ private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12) readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html"))) - private val syslog = new TextArea + private val syslog = new TextArea(Isabelle.session.syslog()) syslog.editable = false private val tabs = new TabbedPane { pages += new TabbedPane.Page("README", Component.wrap(readme)) pages += new TabbedPane.Page("System log", new ScrollPane(syslog)) + + selection.index = + { + val index = Isabelle.Int_Property("session-panel.selection", 0) + if (index >= pages.length) 0 else index + } + listenTo(selection) + reactions += { + case SelectionChanged(_) => + Isabelle.Int_Property("session-panel.selection") = selection.index + } } set_content(tabs) @@ -38,12 +50,17 @@ /* controls */ + val session_phase = new Label(Isabelle.session.phase.toString) + session_phase.border = Swing.EtchedBorder(Swing.Lowered) + session_phase.tooltip = "Prover process status" + private val interrupt = new Button("Interrupt") { reactions += { case ButtonClicked(_) => Isabelle.session.interrupt } } interrupt.tooltip = "Broadcast interrupt to all prover tasks" - private val controls = new FlowPanel(FlowPanel.Alignment.Right)(interrupt) + private val controls = + new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt) add(controls.peer, BorderLayout.NORTH) @@ -53,14 +70,29 @@ loop { react { case result: Isabelle_Process.Result => - if (result.is_init || result.is_exit || result.is_system || result.is_ready) - Swing_Thread.now { syslog.append(XML.content(result.message).mkString + "\n") } + if (result.is_syslog) + Swing_Thread.now { + val text = Isabelle.session.syslog() + if (text != syslog.text) { + syslog.text = text + } + } + + case (_, phase: Session.Phase) => + Swing_Thread.now { session_phase.text = phase.toString } case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) } } } - override def init() { Isabelle.session.raw_messages += main_actor } - override def exit() { Isabelle.session.raw_messages -= main_actor } + override def init() { + Isabelle.session.raw_messages += main_actor + Isabelle.session.phase_changed += main_actor + } + + override def exit() { + Isabelle.session.raw_messages -= main_actor + Isabelle.session.phase_changed -= main_actor + } }