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;
--- 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) {
--- 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())
}
--- 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()
}
--- 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
}
}
}
--- 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("<parser stopped>"))
+ 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("<parser stopped>"))
+ case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
}
- else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
-
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
--- 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, _)
--- 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()
}
}
--- 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
}
--- 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()
}
}
--- 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
- }
-}
--- 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)
}
}
--- 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() }
-}
--- /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 _ =>
+ }
+ //}}}
+ }
+ }
+}
--- 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
}
}
--- 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()
}