# HG changeset patch # User immler@in.tum.de # Date 1237475937 -3600 # Node ID 20bfcca24658d1e81cf2dae00899bad93699a88e # Parent f76e733774386f03db08ea505bbd02a93bb17b58 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 diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- 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) diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- 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); diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/jedit/ProverSetup.scala --- 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 diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/jedit/TheoryView.scala --- 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) diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/proofdocument/DocumentActor.scala --- 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) - } - } - } -} diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- 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) } } diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/prover/Prover.scala --- 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) } } diff -r f76e73377438 -r 20bfcca24658 src/Tools/jEdit/src/utils/LinearSet.scala --- 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