--- 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"
)
--- 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=""
--- 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=""
--- 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
}
}
--- 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]]] =
--- 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 =
--- 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;
--- 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()
}
--- 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 }
--- 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
}
}
--- 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
--- 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
--- 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 @@
<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
<ACTIONS>
- <ACTION NAME="isabelle.activate">
- <CODE>
- isabelle.jedit.Isabelle.switch_active(view);
- </CODE>
- <IS_SELECTED>
- return isabelle.jedit.Isabelle.is_active(view);
- </IS_SELECTED>
- </ACTION>
<ACTION NAME="isabelle.session-panel">
<CODE>
wm.addDockableWindow("isabelle-session");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.show-output">
+ <ACTION NAME="isabelle.output-panel">
<CODE>
wm.addDockableWindow("isabelle-output");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.show-raw-output">
+ <ACTION NAME="isabelle.raw-output-panel">
<CODE>
wm.addDockableWindow("isabelle-raw-output");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.show-protocol">
+ <ACTION NAME="isabelle.protocol-panel">
<CODE>
wm.addDockableWindow("isabelle-protocol");
</CODE>
--- 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)
--- 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)
--- 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]]) { }
+ }
+ }
}
}
}
--- 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
}
}
--- 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
+ }
}