Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
added actor to TheoryView, receiving updates of Commands (removed EventBus command_info);
Prover.edit_document from Makarius 'broken' repository;
LinearSet: fixed prev
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Thu Mar 19 16:18:57 2009 +0100
@@ -7,8 +7,7 @@
package isabelle.jedit
-import isabelle.proofdocument.ProofDocument
-import isabelle.prover.{Command, MarkupNode}
+import isabelle.prover.{Command, MarkupNode, Prover}
import isabelle.Markup
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -68,7 +67,7 @@
}
-class DynamicTokenMarker(buffer: JEditBuffer, document: ProofDocument) extends TokenMarker {
+class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker {
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = {
@@ -83,7 +82,7 @@
var next_x = start
for {
- command <- document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
+ command <- prover.document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
markup <- command.root_node.flatten
if(to(markup.abs_stop) > start)
if(to(markup.abs_start) < stop)
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Thu Mar 19 16:18:57 2009 +0100
@@ -24,7 +24,6 @@
var textarea : JEditTextArea = null
val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
- prover.command_info += (_ => repaint_delay.delay_or_ignore())
setRequestFocusEnabled(false);
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Mar 19 16:18:57 2009 +0100
@@ -9,7 +9,6 @@
import isabelle.prover.{Prover, Command}
import isabelle.renderer.UserAgent
-import isabelle.proofdocument.DocumentActor
import org.w3c.dom.Document
@@ -35,15 +34,13 @@
def activate(view: View) {
prover = new Prover(Isabelle.system, Isabelle.default_logic)
-
+ prover.start() //start actor
val buffer = view.getBuffer
- val dir = buffer.getDirectory
+ val path = buffer.getPath
- val document_actor = new DocumentActor
- document_actor.start
- theory_view = new TheoryView(view.getTextArea, document_actor)
- prover.set_document(document_actor,
- if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
+ theory_view = new TheoryView(view.getTextArea, prover)
+ prover.set_document(theory_view.change_receiver,
+ if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path)
theory_view.activate
//register output-view
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Mar 19 16:18:57 2009 +0100
@@ -87,7 +87,7 @@
phase_overview.textarea = text_area
text_area.addLeftOfScrollBar(phase_overview)
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
- buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
+ buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
update_styles
document_actor ! new Text.Change(0,buffer.getText(0, buffer.getLength),0)
}
@@ -102,7 +102,17 @@
/* painting */
val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
- prover.command_info += (_ => repaint_delay.delay_or_ignore())
+
+ val change_receiver = scala.actors.Actor.actor {
+ scala.actors.Actor.loop {
+ scala.actors.Actor.react {
+ case _ => {
+ repaint_delay.delay_or_ignore()
+ phase_overview.repaint_delay.delay_or_ignore()
+ }
+ }
+ }
+ }.start
def from_current (pos: Int) =
if (col != null && col.start <= pos)
--- a/src/Tools/jEdit/src/proofdocument/DocumentActor.scala Thu Mar 19 13:16:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-/*
- * Managing changes on ProofDocuments via Actors
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.proofdocument
-
-import scala.actors.Actor
-import scala.actors.Actor._
-import isabelle.utils.LinearSet
-
-object DocumentActor {
- case class Activate
- case class SetEventBus(bus: EventBus[StructureChange])
- case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
-}
-class DocumentActor extends Actor {
- private var versions = List(
- new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false, new EventBus))
-
- def get = versions.head
-
- def act() {
- import DocumentActor._
- loop {
- react {
- case Activate => versions ::= versions.head.activate
- case SetEventBus(bus) => versions ::= versions.head.set_event_bus(bus)
- case SetIsCommandKeyword(f) => versions ::= versions.head.set_command_keyword(f)
- case change: Text.Change => versions ::= versions.head.text_changed(change)
- }
- }
- }
-}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Mar 19 16:18:57 2009 +0100
@@ -38,26 +38,28 @@
"`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
"[()\\[\\]{}:;]", Pattern.MULTILINE)
+ val empty = new ProofDocument(LinearSet.empty, LinearSet.empty, false, _ => false)
+
}
class ProofDocument(val tokens: LinearSet[Token],
val commands: LinearSet[Command],
val active: Boolean,
- is_command_keyword: String => Boolean,
- structural_changes: EventBus[StructureChange])
+ is_command_keyword: String => Boolean)
{
- def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword, structural_changes)
- def activate: ProofDocument = text_changed(new Text.Change(0, content, content.length)).mark_active
+ def mark_active: ProofDocument = new ProofDocument(tokens, commands, true, is_command_keyword)
+ def activate: (ProofDocument, StructureChange) = {
+ val (doc, change) = text_changed(new Text.Change(0, content, content.length))
+ return (doc.mark_active, change)
+ }
def set_command_keyword(f: String => Boolean): ProofDocument =
- new ProofDocument(tokens, commands, active, f, structural_changes)
- def set_event_bus(bus: EventBus[StructureChange]): ProofDocument =
- new ProofDocument(tokens, commands, active, is_command_keyword, bus)
+ new ProofDocument(tokens, commands, active, f)
def content = Token.string_from_tokens(List() ++ tokens)
/** token view **/
- def text_changed(change: Text.Change): ProofDocument =
+ def text_changed(change: Text.Change): (ProofDocument, StructureChange) =
{
val tokens = List() ++ this.tokens
val (begin, remaining) = tokens.span(_.stop < change.start)
@@ -123,7 +125,7 @@
inserted_tokens: List[Token],
removed_tokens: List[Token],
new_tokenset: LinearSet[Token],
- after_change: Option[Token]): ProofDocument =
+ after_change: Option[Token]): (ProofDocument, StructureChange) =
{
val commands = List() ++ this.commands
val (begin, remaining) =
@@ -163,13 +165,13 @@
}
}
- System.err.println("ins_tokens: " + inserted_tokens)
val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
- System.err.println("new_commands: " + new_commands)
val new_commandset = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
val before = begin match {case Nil => None case _ => Some (begin.last)}
- structural_changes.event(new StructureChange(before, new_commands, removed))
- new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword, structural_changes)
+
+ val change = new StructureChange(before, new_commands, removed)
+ val doc = new ProofDocument(new_tokenset, new_commandset, active, is_command_keyword)
+ return (doc, change)
}
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Mar 19 16:18:57 2009 +0100
@@ -12,23 +12,31 @@
import scala.collection.mutable
import scala.collection.immutable.{TreeSet}
+import scala.actors.Actor
+import scala.actors.Actor._
+
import org.gjt.sp.util.Log
import isabelle.jedit.Isabelle
-import isabelle.proofdocument.{DocumentActor, ProofDocument, Text, Token}
+import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token}
import isabelle.IsarDocument
+object ProverEvents {
+ case class Activate
+ case class SetEventBus(bus: EventBus[StructureChange])
+ case class SetIsCommandKeyword(is_command_keyword: String => Boolean)
+}
-class Prover(isabelle_system: IsabelleSystem, logic: String)
+class Prover(isabelle_system: IsabelleSystem, logic: String) extends Actor
{
/* prover process */
- private var process: Isar = null
+ private var process: Isar with IsarDocument= null
{
val results = new EventBus[IsabelleProcess.Result] + handle_result
results.logger = Log.log(Log.ERROR, null, _)
- process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
+ process = new Isar(isabelle_system, results, "-m", "xsymbols", logic) with IsarDocument
}
def stop() { process.kill }
@@ -39,7 +47,10 @@
private val states = new mutable.HashMap[IsarDocument.State_ID, Command]
private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command]
private val document0 = Isabelle.plugin.id()
- private val document_versions = new mutable.HashSet[IsarDocument.Document_ID] + document0
+ private var document_versions = List((document0, ProofDocument.empty))
+
+ def get_id = document_versions.head._1
+ def document = document_versions.head._2
private var initialized = false
@@ -79,12 +90,10 @@
/* event handling */
val activated = new EventBus[Unit]
- val command_info = new EventBus[Command]
val output_info = new EventBus[String]
- var document_actor: DocumentActor = null
- def document = document_actor.get
-
- def command_change(c: Command) = Swing.now { command_info.event(c) }
+ var change_receiver = null: Actor
+
+ def command_change(c: Command) = this ! c
private def handle_result(result: IsabelleProcess.Result)
{
@@ -101,18 +110,21 @@
Swing.now { output_info.event(result.result) }
else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) { // FIXME !?
initialized = true
- Swing.now { document_actor ! DocumentActor.Activate }
+ Swing.now { this ! ProverEvents.Activate }
}
else {
result.kind match {
case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
- | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR
- if command != null =>
- if (result.kind == IsabelleProcess.Kind.ERROR)
- command.status = Command.Status.FAILED
- command.add_result(running, process.parse_message(result))
- command_change(command)
+ | IsabelleProcess.Kind.WARNING | IsabelleProcess.Kind.ERROR =>
+ if (command != null) {
+ if (result.kind == IsabelleProcess.Kind.ERROR)
+ command.status = Command.Status.FAILED
+ command.add_result(running, process.parse_message(result))
+ command_change(command)
+ } else {
+ output_info.event(result.toString)
+ }
case IsabelleProcess.Kind.STATUS =>
//{{{ handle all kinds of status messages here
@@ -136,13 +148,13 @@
<- edits
if (commands.contains(cmd_id))
} {
- val cmd = commands(cmd_id)
- if (cmd.state_id != null) states -= cmd.state_id
- states(cmd_id) = cmd
- cmd.state_id = state_id
- cmd.status = Command.Status.UNPROCESSED
- command_change(cmd)
- }
+ val cmd = commands(cmd_id)
+ if (cmd.state_id != null) states -= cmd.state_id
+ states(cmd_id) = cmd
+ cmd.state_id = state_id
+ cmd.status = Command.Status.UNPROCESSED
+ command_change(cmd)
+ }
// command status
case XML.Elem(Markup.UNPROCESSED, _, _)
@@ -170,9 +182,10 @@
if (command == null) commands.getOrElse(markup_id, null)
// inner syntax: id from props
else command
- if (cmd != null)
+ if (cmd != null) {
cmd.root_node.insert(cmd.node_from(kind, begin, end))
-
+ command_change(cmd)
+ }
case _ =>
//}}}
}
@@ -186,33 +199,59 @@
}
}
- def set_document(document_actor: isabelle.proofdocument.DocumentActor, path: String) {
- val structural_changes = new EventBus[isabelle.proofdocument.StructureChange]
-
- this.document_actor = document_actor
- document_actor ! DocumentActor.SetEventBus(structural_changes)
- document_actor ! DocumentActor.SetIsCommandKeyword(command_decls.contains)
-
- process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
-
- structural_changes += (changes => if(initialized){
- for (cmd <- changes.removed_commands) remove(cmd)
- changes.added_commands.foldLeft (changes.before_change) ((p, c) => {send(p, c); Some(c)})
- })
+ def act() {
+ import ProverEvents._
+ loop {
+ react {
+ case Activate => {
+ val (doc, structure_change) = document.activate
+ val old_id = get_id
+ val doc_id = Isabelle.plugin.id()
+ document_versions ::= (doc_id, doc)
+ edit_document(old_id, doc_id, structure_change)
+ }
+ case SetIsCommandKeyword(f) => {
+ val old_id = get_id
+ val doc_id = Isabelle.plugin.id()
+ document_versions ::= (doc_id, document.set_command_keyword(f))
+ edit_document(old_id, doc_id, StructureChange(None, Nil, Nil))
+ }
+ case change: Text.Change => {
+ val (doc, structure_change) = document.text_changed(change)
+ val old_id = get_id
+ val doc_id = Isabelle.plugin.id()
+ document_versions ::= (doc_id, doc)
+ edit_document(old_id, doc_id, structure_change)
+ }
+ case command: Command => {
+ //state of command has changed
+ change_receiver ! command
+ }
+ }
+ }
+ }
+
+ def set_document(change_receiver: Actor, path: String) {
+ this.change_receiver = change_receiver
+ this ! ProverEvents.SetIsCommandKeyword(command_decls.contains)
+ process.ML("()") // FIXME force initial writeln
+ process.begin_document(document0, path)
}
- private def send(prev: Option[Command], cmd: Command) {
- cmd.status = Command.Status.UNPROCESSED
- commands.put(cmd.id, cmd)
-
- val content = isabelle_system.symbols.encode(cmd.content)
- process.create_command(cmd.id, content)
- process.insert_command(prev match {case Some(c) => c.id case None => ""}, cmd.id)
- }
-
- def remove(cmd: Command) {
- commands -= cmd.id
- if (cmd.state_id != null) states -= cmd.state_id
- process.remove_command(cmd.id)
+ private def edit_document(old_id: String, document_id: String, changes: StructureChange) = Swing.now
+ {
+ val removes =
+ for (cmd <- changes.removed_commands) yield {
+ commands -= cmd.id
+ if (cmd.state_id != null) states -= cmd.state_id
+ (document.commands.prev(cmd).map(_.id).getOrElse(document0)) -> None
+ }
+ val inserts =
+ for (cmd <- changes.added_commands) yield {
+ commands += (cmd.id -> cmd)
+ process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content))
+ (document.commands.prev(cmd).map(_.id).getOrElse(document0)) -> Some(cmd.id)
+ }
+ process.edit_document(old_id, document_id, removes.reverse ++ inserts)
}
}
--- a/src/Tools/jEdit/src/utils/LinearSet.scala Thu Mar 19 13:16:07 2009 +0100
+++ b/src/Tools/jEdit/src/utils/LinearSet.scala Thu Mar 19 16:18:57 2009 +0100
@@ -34,7 +34,7 @@
/* basic methods */
def next(elem: A) = body.get(elem)
- def prev(elem: A) = body.find(_._2 == elem).map(_._2)
+ def prev(elem: A) = body.find(_._2 == elem).map(_._1)
override def isEmpty: Boolean = !last_elem.isDefined
def size: Int = if (isEmpty) 0 else body.size + 1