# HG changeset patch # User wenzelm # Date 1260479719 -3600 # Node ID 91d6089cef88bb971cede4a399bc599710b5a1b5 # Parent 01a9bfd64b8702af93fcfa607c368e4710be4c32 class Session models full session, with or without prover process (cf. heaps, browser_info); replaced Prover by Session, with a singleton instance in Isabelle plugin (shared by all active buffers); misc cleanup of Session vs. Plugin instance; eliminated Prover_Setup -- maintain mapping of JEditBuffer <-> Theory_View directly; misc tuning and simplification; diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/document_overview.scala --- a/src/Tools/jEdit/src/jedit/document_overview.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/document_overview.scala Thu Dec 10 22:15:19 2009 +0100 @@ -7,7 +7,7 @@ package isabelle.jedit -import isabelle.proofdocument.{Command, Proof_Document, Prover, Theory_View} +import isabelle.proofdocument.{Command, Proof_Document, Theory_View} import javax.swing.{JPanel, ToolTipManager} import java.awt.event.{MouseAdapter, MouseEvent} @@ -15,11 +15,9 @@ import org.gjt.sp.jedit.gui.RolloverButton import org.gjt.sp.jedit.textarea.JEditTextArea -import org.gjt.sp.jedit.buffer.JEditBuffer class Document_Overview( - prover: Prover, text_area: JEditTextArea, to_current: (Proof_Document, Int) => Int) extends JPanel(new BorderLayout) @@ -56,10 +54,11 @@ else "" } - override def paintComponent(gfx: Graphics) { + override def paintComponent(gfx: Graphics) + { super.paintComponent(gfx) val buffer = text_area.getBuffer - val theory_view = Isabelle.prover_setup(buffer).get.theory_view + val theory_view = Isabelle.plugin.theory_view(buffer).get val doc = theory_view.current_document() for (command <- doc.commands) { diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/history_dockable.scala --- a/src/Tools/jEdit/src/jedit/history_dockable.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/history_dockable.scala Thu Dec 10 22:15:19 2009 +0100 @@ -7,7 +7,7 @@ package isabelle.jedit -import isabelle.proofdocument.Change +import isabelle.proofdocument.{Change, Theory_View} import java.awt.Dimension import scala.swing.{ListView, FlowPanel} @@ -22,11 +22,12 @@ if (position == DockableWindowManager.FLOATING) preferredSize = new Dimension(500, 250) - def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer) + def dynamic_theory_view(): Option[Theory_View] = + Isabelle.plugin.theory_view(view.getBuffer) def get_versions() = - prover_setup() match { + dynamic_theory_view() match { case None => Nil - case Some(setup) => setup.theory_view.changes + case Some(theory_view) => theory_view.changes } val list = new ListView[Change] @@ -37,8 +38,9 @@ listenTo(list.selection) reactions += { case ListSelectionChanged(source, range, false) => - prover_setup().map(_.theory_view.set_version(list.listData(range.start))) + dynamic_theory_view().map(_.set_version(list.listData(range.start))) } - prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions())) + if (dynamic_theory_view().isDefined) + Isabelle.session.document_change += (_ => list.listData = get_versions()) } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/isabelle_encoding.scala --- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Thu Dec 10 22:15:19 2009 +0100 @@ -34,7 +34,7 @@ { def source(): Source = BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() }) - new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray) + new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray) } override def getTextReader(in: InputStream): Reader = @@ -53,7 +53,7 @@ val buffer = new ByteArrayOutputStream(BUFSIZE) { override def flush() { - val text = Isabelle.symbols.encode(toString(Isabelle_System.charset)) + val text = Isabelle.system.symbols.encode(toString(Isabelle_System.charset)) out.write(text.getBytes(Isabelle_System.charset)) out.flush() } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Dec 10 22:15:19 2009 +0100 @@ -45,38 +45,35 @@ { def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = { - val prover = Isabelle.prover_setup(buffer).map(_.prover) - val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view) - if (prover.isEmpty || theory_view_opt.isEmpty) null - else if (prover.get == null || theory_view_opt.get == null) null - else { - val theory_view = theory_view_opt.get - val document = theory_view.current_document() - val offset = theory_view.from_current(document, original_offset) - document.command_at(offset) match { - case Some(command) => - command.ref_at(document, offset - command.start(document)) match { - case Some(ref) => - val command_start = command.start(document) - val begin = theory_view.to_current(document, command_start + ref.start) - val line = buffer.getLineOfOffset(begin) - val end = theory_view.to_current(document, command_start + ref.stop) - ref.info match { - case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => - new External_Hyperlink(begin, end, line, ref_file, ref_line) - case Command.RefInfo(_, _, Some(id), Some(offset)) => - prover.get.command(id) match { - case Some(ref_cmd) => - new Internal_Hyperlink(begin, end, line, - theory_view.to_current(document, ref_cmd.start(document) + offset - 1)) - case None => null - } - case _ => null - } - case None => null - } - case None => null - } + Isabelle.plugin.theory_view(buffer) match { + case Some(theory_view) => + val document = theory_view.current_document() + val offset = theory_view.from_current(document, original_offset) + document.command_at(offset) match { + case Some(command) => + command.ref_at(document, offset - command.start(document)) match { + case Some(ref) => + val command_start = command.start(document) + val begin = theory_view.to_current(document, command_start + ref.start) + val line = buffer.getLineOfOffset(begin) + val end = theory_view.to_current(document, command_start + ref.stop) + ref.info match { + case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => + new External_Hyperlink(begin, end, line, ref_file, ref_line) + case Command.RefInfo(_, _, Some(id), Some(offset)) => + Isabelle.session.command(id) match { + case Some(ref_cmd) => + new Internal_Hyperlink(begin, end, line, + theory_view.to_current(document, ref_cmd.start(document) + offset - 1)) + case None => null + } + case _ => null + } + case None => null + } + case None => null + } + case None => null } } } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Dec 10 22:15:19 2009 +0100 @@ -40,38 +40,37 @@ val root = data.root data.getAsset(root).setEnd(buffer.getLength) - val prover_setup = Isabelle.prover_setup(buffer) - if (prover_setup.isDefined) { - val document = prover_setup.get.theory_view.current_document() - for (command <- document.commands if !stopped) { - root.add(command.markup_root(document).swing_tree((node: Markup_Node) => - { - val content = command.content(node.start, node.stop) - val command_start = command.start(document) - val id = command.id + Isabelle.plugin.theory_view(buffer) match { + case Some(theory_view) => + val document = theory_view.current_document() + for (command <- document.commands if !stopped) { + root.add(command.markup_root(document).swing_tree((node: Markup_Node) => + { + val content = command.content(node.start, node.stop) + val command_start = command.start(document) + val id = command.id - new DefaultMutableTreeNode(new IAsset { - override def getIcon: Icon = null - override def getShortString: String = content - override def getLongString: String = node.info.toString - override def getName: String = id - override def setName(name: String) = () - override def setStart(start: Position) = () - override def getStart: Position = command_start + node.start - override def setEnd(end: Position) = () - override def getEnd: Position = command_start + node.stop - override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]" - }) - })) - } - if (stopped) root.add(new DefaultMutableTreeNode("")) + new DefaultMutableTreeNode(new IAsset { + override def getIcon: Icon = null + override def getShortString: String = content + override def getLongString: String = node.info.toString + override def getName: String = id + override def setName(name: String) = () + override def setStart(start: Position) = () + override def getStart: Position = command_start + node.start + override def setEnd(end: Position) = () + override def getEnd: Position = command_start + node.stop + override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]" + }) + })) + } + if (stopped) root.add(new DefaultMutableTreeNode("")) + case None => root.add(new DefaultMutableTreeNode("")) } - else root.add(new DefaultMutableTreeNode("")) - data } - + /* completion */ override def supportsCompletion = true @@ -85,8 +84,7 @@ val start = buffer.getLineStartOffset(line) val text = buffer.getSegment(start, caret - start) - val completion = - Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion) + val completion = Isabelle.session.completion() completion.complete(text) match { case None => null diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Dec 10 22:15:19 2009 +0100 @@ -8,7 +8,6 @@ package isabelle.jedit -import isabelle.proofdocument.Prover import isabelle.Markup import org.gjt.sp.jedit.buffer.JEditBuffer @@ -100,7 +99,7 @@ } -class Isabelle_Token_Marker(buffer: JEditBuffer, prover: Prover) extends TokenMarker +class Isabelle_Token_Marker(buffer: JEditBuffer) extends TokenMarker { override def markTokens(prev: TokenMarker.LineContext, handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = @@ -111,7 +110,7 @@ val start = buffer.getLineStartOffset(line) val stop = start + line_segment.count - val theory_view = Isabelle.prover_setup(buffer).get.theory_view + val theory_view = Isabelle.plugin.theory_view(buffer).get // FIXME total? val document = theory_view.current_document() def to: Int => Int = theory_view.to_current(document, _) def from: Int => Int = theory_view.from_current(document, _) diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Dec 10 22:15:19 2009 +0100 @@ -42,11 +42,15 @@ loop { react { case cmd: Command => - val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view - val body = - if (cmd == null) Nil // FIXME ?? - else cmd.results(theory_view.current_document) - html_panel.render(body) + Isabelle.plugin.theory_view(view.getBuffer) // FIXME total!?! + match { + case None => + case Some(theory_view) => + val body = + if (cmd == null) Nil // FIXME ?? + else cmd.results(theory_view.current_document) + html_panel.render(body) + } case bad => System.err.println("output_actor: ignoring bad message " + bad) } @@ -62,15 +66,17 @@ } } - override def addNotify() { + override def addNotify() + { super.addNotify() - Isabelle.plugin.state_update += output_actor - Isabelle.plugin.properties_changed += properties_actor + Isabelle.session.results += output_actor + Isabelle.session.global_settings += properties_actor } - override def removeNotify() { - Isabelle.plugin.state_update -= output_actor - Isabelle.plugin.properties_changed -= properties_actor + override def removeNotify() + { + Isabelle.session.results -= output_actor + Isabelle.session.global_settings -= properties_actor super.removeNotify() } } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Thu Dec 10 22:15:19 2009 +0100 @@ -9,15 +9,14 @@ package isabelle.jedit +import isabelle.proofdocument.{Session, Theory_View} + import java.io.{FileInputStream, IOException} import java.awt.Font import javax.swing.JScrollPane import scala.collection.mutable -import isabelle.proofdocument.{Command, Proof_Document, Prover} -import isabelle.Isabelle_System - import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.textarea.JEditTextArea @@ -54,16 +53,9 @@ } - /* Isabelle system instance */ - - var system: Isabelle_System = null - def symbols = system.symbols - lazy val completion = new Completion + symbols - - /* settings */ - def default_logic(): String = + def get_logic(): String = { val logic = Isabelle.Property("logic") if (logic != null) logic @@ -74,51 +66,44 @@ /* plugin instance */ var plugin: Plugin = null - - - /* running provers */ - - def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer) + var system: Isabelle_System = null + var session: Session = null } class Plugin extends EBPlugin { - /* event buses */ - - val properties_changed = new Event_Bus[Unit] - val raw_results = new Event_Bus[Isabelle_Process.Result] - val state_update = new Event_Bus[Command] - - - /* selected state */ + /* mapping buffer <-> theory view */ - private var _selected_state: Command = null - def selected_state = _selected_state - def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) } - - - /* mapping buffer <-> prover */ - - private val mapping = new mutable.HashMap[JEditBuffer, Prover_Setup] + private var mapping = Map[JEditBuffer, Theory_View]() private def install(view: View) { + val text_area = view.getTextArea val buffer = view.getBuffer - val prover_setup = new Prover_Setup(buffer) - mapping.update(buffer, prover_setup) - prover_setup.activate(view) + + + val theory_view = new Theory_View(Isabelle.session, text_area) // FIXME multiple text areas!? + mapping += (buffer -> theory_view) + + Isabelle.session.start(Isabelle.get_logic()) + theory_view.activate() + Isabelle.session.begin_document(buffer.getName) } - private def uninstall(view: View) = - mapping.removeKey(view.getBuffer).get.deactivate + private def uninstall(view: View) + { + val buffer = view.getBuffer + mapping(buffer).deactivate + mapping -= buffer + } def switch_active(view: View) = if (mapping.isDefinedAt(view.getBuffer)) uninstall(view) else install(view) - def prover_setup(buffer: JEditBuffer): Option[Prover_Setup] = mapping.get(buffer) - def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer) + def theory_view(buffer: JEditBuffer): Option[Theory_View] = mapping.get(buffer) + def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer) /* main plugin plumbing */ @@ -130,13 +115,14 @@ val buffer = msg.getEditPane.getBuffer msg.getWhat match { case EditPaneUpdate.BUFFER_CHANGED => - (mapping get buffer) map (_.theory_view.activate) + theory_view(buffer)map(_.activate) case EditPaneUpdate.BUFFER_CHANGING => if (buffer != null) - (mapping get buffer) map (_.theory_view.deactivate) + theory_view(buffer).map(_.deactivate) case _ => } - case msg: PropertiesChanged => properties_changed.event(()) + case msg: PropertiesChanged => + Isabelle.session.global_settings.event(()) case _ => } } @@ -146,11 +132,13 @@ Isabelle.plugin = this Isabelle.system = new Isabelle_System Isabelle.system.install_fonts() + Isabelle.session = new Session(Isabelle.system) // FIXME dialog!? } override def stop() { - // TODO: proper cleanup + Isabelle.session.stop() // FIXME dialog!? + Isabelle.session = null Isabelle.system = null Isabelle.plugin = null } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/protocol_dockable.scala --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu Dec 10 22:15:19 2009 +0100 @@ -48,12 +48,12 @@ override def addNotify() { super.addNotify() - Isabelle.plugin.raw_results += raw_actor + Isabelle.session.raw_results += raw_actor } override def removeNotify() { - Isabelle.plugin.raw_results -= raw_actor + Isabelle.session.raw_results -= raw_actor super.removeNotify() } } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/jedit/prover_setup.scala --- a/src/Tools/jEdit/src/jedit/prover_setup.scala Thu Dec 10 14:23:28 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -/* - * Independent prover sessions for each buffer - * - * @author Fabian Immler, TU Munich - */ - -package isabelle.jedit - - -import org.gjt.sp.jedit.{Buffer, View} - -import isabelle.proofdocument.{Prover, Theory_View} - - -class Prover_Setup(buffer: Buffer) -{ - var prover: Prover = null - var theory_view: Theory_View = null - - def activate(view: View) - { - // Theory_View starts prover - theory_view = new Theory_View(view.getTextArea) - prover = theory_view.prover - - theory_view.activate() - prover.begin_document(buffer.getName) - } - - def deactivate() - { - theory_view.deactivate - prover.stop - } -} diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/proofdocument/command.scala --- a/src/Tools/jEdit/src/proofdocument/command.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/command.scala Thu Dec 10 22:15:19 2009 +0100 @@ -12,7 +12,7 @@ import scala.collection.mutable -import isabelle.jedit.{Isabelle, Plugin} +import isabelle.jedit.Isabelle import isabelle.XML @@ -26,7 +26,7 @@ override def act() { loop { react { - case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message) + case (session: Session, message: XML.Tree) => _state = _state.+(session, message) case bad => System.err.println("Accumulator: ignoring bad message " + bad) } } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/proofdocument/prover.scala --- a/src/Tools/jEdit/src/proofdocument/prover.scala Thu Dec 10 14:23:28 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,170 +0,0 @@ -/* - * Higher-level prover communication: interactive document model - * - * @author Johannes Hölzl, TU Munich - * @author Fabian Immler, TU Munich - * @author Makarius - */ - -package isabelle.proofdocument - - -import scala.actors.Actor, Actor._ - -import javax.swing.JTextArea - -import isabelle.jedit.Isabelle - - -class Prover(system: Isabelle_System, logic: String) -{ - /* incoming messages */ - - private var prover_ready = false - - private val receiver = new Actor { - def act() { - loop { - react { - case result: Isabelle_Process.Result => handle_result(result) - case change: Change if prover_ready => handle_change(change) - case bad if prover_ready => System.err.println("receiver: ignoring bad message " + bad) - } - } - } - } - - def input(change: Change) { receiver ! change } - - - /* outgoing messages */ - - val command_change = new Event_Bus[Command] - val document_change = new Event_Bus[Proof_Document] - - - /* prover process */ - - private val process = - new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document - - - /* outer syntax keywords and completion */ - - @volatile private var _command_decls = Map[String, String]() - def command_decls() = _command_decls - - @volatile private var _keyword_decls = Set[String]() - def keyword_decls() = _keyword_decls - - @volatile private var _completion = Isabelle.completion - def completion() = _completion - - - /* document state information */ - - @volatile private var states = Map[Isar_Document.State_ID, Command_State]() - @volatile private var commands = Map[Isar_Document.Command_ID, Command]() - val document_0 = - Proof_Document.empty. - set_command_keyword((s: String) => command_decls().contains(s)) - @volatile private var document_versions = List(document_0) - - def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) - def document(id: Isar_Document.Document_ID): Option[Proof_Document] = - document_versions.find(_.id == id) - - - /* prover results */ - - private def handle_result(result: Isabelle_Process.Result) - { - Isabelle.plugin.raw_results.event(result) - val message = Isabelle_Process.parse_message(system, result) - - val state = - Position.id_of(result.props) match { - case None => None - case Some(id) => commands.get(id) orElse states.get(id) orElse None - } - if (state.isDefined) state.get ! (this, message) - else if (result.kind == Isabelle_Process.Kind.STATUS) { - //{{{ global status message - message match { - case XML.Elem(Markup.MESSAGE, _, elems) => - for (elem <- elems) { - elem match { - // document edits - case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => - document_versions.find(_.id == doc_id) match { - case Some(doc) => - for { - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) - <- edits } - { - commands.get(cmd_id) match { - case Some(cmd) => - val state = new Command_State(cmd) - states += (state_id -> state) - doc.states += (cmd -> state) - command_change.event(cmd) // FIXME really!? - case None => - } - } - case None => - } - - // command and keyword declarations - case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => - _command_decls += (name -> kind) - _completion += name - case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => - _keyword_decls += name - _completion += name - - // process ready (after initialization) - case XML.Elem(Markup.READY, _, _) => prover_ready = true - - case _ => - } - } - case _ => - } - //}}} - } - } - - - /* document changes */ - - def begin_document(path: String) { - process.begin_document(document_0.id, path) - } - - def handle_change(change: Change) { - val old = document(change.parent.get.id).get - val (doc, changes) = old.text_changed(change) - document_versions ::= doc - - val id_changes = changes map { case (c1, c2) => - (c1.map(_.id).getOrElse(document_0.id), - c2 match { - case None => None - case Some(command) => - commands += (command.id -> command) - process.define_command(command.id, system.symbols.encode(command.content)) - Some(command.id) - }) - } - process.edit_document(old.id, doc.id, id_changes) - - document_change.event(doc) - } - - - /* main controls */ - - def start() { receiver.start() } - - def stop() { process.kill() } -} diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/proofdocument/session.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/session.scala Thu Dec 10 22:15:19 2009 +0100 @@ -0,0 +1,192 @@ +/* + * Isabelle session, potentially with running prover + * + * @author Makarius + */ + +package isabelle.proofdocument + + +import scala.actors.Actor._ + + +class Session(system: Isabelle_System) +{ + /* main actor */ + + private case class Start(logic: String) + private case object Stop + + private var prover: Isabelle_Process with Isar_Document = null + private var prover_logic = "" + private var prover_ready = false + + private val session_actor = actor { + loop { + react { + case Start(logic) => + if (prover == null) { + // FIXME only once + prover = // FIXME rebust error handling (via results) + new Isabelle_Process(system, self, // FIXME improve options + "-m", "xsymbols", "-m", "no_brackets", "-m", "no_type_brackets", logic) + with Isar_Document + prover_logic = logic + reply(()) + } + + case Stop => + if (prover != null) + prover.kill + prover = null // FIXME later (via results)!? + prover_ready = false // FIXME !?? + + case change: Change if prover_ready => + handle_change(change) + + case result: Isabelle_Process.Result => + handle_result(result) + + case bad if prover_ready => + System.err.println("session_actor: ignoring bad message " + bad) + } + } + } + + def start(logic: String) { session_actor !? Start(logic) } + def stop() { session_actor ! Stop } + def input(change: Change) { session_actor ! change } + + + /* pervasive event buses */ + + val global_settings = new Event_Bus[Unit] + val raw_results = new Event_Bus[Isabelle_Process.Result] + val results = new Event_Bus[Command] + + val command_change = new Event_Bus[Command] + val document_change = new Event_Bus[Proof_Document] + + + /* selected state */ // FIXME!? races!? + + private var _selected_state: Command = null + def selected_state = _selected_state + def selected_state_=(state: Command) { _selected_state = state; results.event(state) } + + + /* outer syntax keywords and completion */ + + @volatile private var _command_decls = Map[String, String]() + def command_decls() = _command_decls + + @volatile private var _keyword_decls = Set[String]() + def keyword_decls() = _keyword_decls + + @volatile private var _completion = new Completion + system.symbols + def completion() = _completion + + + /* document state information */ + + @volatile private var states = Map[Isar_Document.State_ID, Command_State]() + @volatile private var commands = Map[Isar_Document.Command_ID, Command]() + val document_0 = + Proof_Document.empty. + set_command_keyword((s: String) => command_decls().contains(s)) // FIXME !? + @volatile private var document_versions = List(document_0) + + def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) + def document(id: Isar_Document.Document_ID): Option[Proof_Document] = + document_versions.find(_.id == id) + + + /* document changes */ + + def begin_document(path: String) + { + prover.begin_document(document_0.id, path) // FIXME fresh id!?! + } + + def handle_change(change: Change) + { + val old = document(change.parent.get.id).get + val (doc, changes) = old.text_changed(change) + document_versions ::= doc + + val id_changes = changes map { + case (c1, c2) => + (c1.map(_.id).getOrElse(document_0.id), + c2 match { + case None => None + case Some(command) => + commands += (command.id -> command) + prover.define_command(command.id, system.symbols.encode(command.content)) + Some(command.id) + }) + } + prover.edit_document(old.id, doc.id, id_changes) + + document_change.event(doc) + } + + + /* prover results */ + + private def handle_result(result: Isabelle_Process.Result) + { + raw_results.event(result) + val message = Isabelle_Process.parse_message(system, result) + + val state = + Position.id_of(result.props) match { + case None => None + case Some(id) => commands.get(id) orElse states.get(id) orElse None + } + if (state.isDefined) state.get ! (this, message) + else if (result.kind == Isabelle_Process.Kind.STATUS) { + //{{{ global status message + message match { + case XML.Elem(Markup.MESSAGE, _, elems) => + for (elem <- elems) { + elem match { + // document edits + case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => + document_versions.find(_.id == doc_id) match { + case Some(doc) => + for { + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) + <- edits } + { + commands.get(cmd_id) match { + case Some(cmd) => + val state = new Command_State(cmd) + states += (state_id -> state) + doc.states += (cmd -> state) + command_change.event(cmd) // FIXME really!? + case None => + } + } + case None => + } + + // command and keyword declarations + case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => + _command_decls += (name -> kind) + _completion += name + case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => + _keyword_decls += name + _completion += name + + // process ready (after initialization) + case XML.Elem(Markup.READY, _, _) => prover_ready = true + + case _ => + } + } + case _ => + } + //}}} + } + } +} diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/proofdocument/state.scala --- a/src/Tools/jEdit/src/proofdocument/state.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/state.scala Thu Dec 10 22:15:19 2009 +0100 @@ -70,7 +70,7 @@ /* message dispatch */ - def + (prover: Prover, message: XML.Tree): State = + def + (session: Session, message: XML.Tree): State = { val changed: State = message match { @@ -111,7 +111,7 @@ }) case _ => add_result(message) } - if (!(this eq changed)) prover.command_change.event(command) + if (!(this eq changed)) session.command_change.event(command) changed } } diff -r 01a9bfd64b87 -r 91d6089cef88 src/Tools/jEdit/src/proofdocument/theory_view.scala --- a/src/Tools/jEdit/src/proofdocument/theory_view.scala Thu Dec 10 14:23:28 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala Thu Dec 10 22:15:19 2009 +0100 @@ -19,7 +19,7 @@ import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle} -import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker} +import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker} // FIXME wrong layer object Theory_View @@ -36,16 +36,14 @@ } -class Theory_View(text_area: JEditTextArea) +class Theory_View(session: Session, text_area: JEditTextArea) { private val buffer = text_area.getBuffer /* prover setup */ - val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic()) - - prover.command_change += ((command: Command) => + session.command_change += ((command: Command) => if (current_document().commands.contains(command)) Swing_Thread.later { // FIXME proper handling of buffer vs. text areas @@ -60,7 +58,7 @@ /* changes vs. edits */ - private val change_0 = new Change(prover.document_0.id, None, Nil) + private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil) // FIXME !? private var _changes = List(change_0) // owned by Swing/AWT thread def changes = _changes private var current_change = change_0 @@ -71,7 +69,7 @@ if (!edits.isEmpty) { val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList) _changes ::= change - prover.input(change) + session.input(change) current_change = change edits.clear } @@ -151,7 +149,7 @@ /* activation */ - private val overview = new Document_Overview(prover, text_area, to_current) + private val overview = new Document_Overview(text_area, to_current) private val selected_state_controller = new CaretListener { override def caretUpdate(e: CaretEvent) { @@ -159,8 +157,8 @@ doc.command_at(e.getDot) match { case Some(cmd) if (doc.token_start(cmd.tokens.first) <= e.getDot && - Isabelle.plugin.selected_state != cmd) => - Isabelle.plugin.selected_state = cmd + Isabelle.session.selected_state != cmd) => + Isabelle.session.selected_state = cmd case _ => } } @@ -172,7 +170,7 @@ text_area.addLeftOfScrollBar(overview) text_area.getPainter. addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension) - buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover)) + buffer.setTokenMarker(new Isabelle_Token_Marker(buffer)) buffer.addBufferListener(buffer_listener) buffer.propertiesChanged() } @@ -190,7 +188,7 @@ /* history of changes */ private def doc_or_pred(c: Change): Proof_Document = - prover.document(c.id).getOrElse(doc_or_pred(c.parent.get)) + session.document(c.id).getOrElse(doc_or_pred(c.parent.get)) def current_document() = doc_or_pred(current_change) @@ -282,8 +280,8 @@ val (start, stop) = lines_of_command(cmd) text_area.invalidateLineRange(start, stop) - if (Isabelle.plugin.selected_state == cmd) - Isabelle.plugin.selected_state = cmd // update State view + if (Isabelle.session.selected_state == cmd) + Isabelle.session.selected_state = cmd } private def invalidate_all() = @@ -313,8 +311,6 @@ /* init */ - prover.start() - edits += Insert(0, buffer.getText(0, buffer.getLength)) edits_delay() }