# HG changeset patch # User immler@in.tum.de # Date 1236549829 -3600 # Node ID aaafe9c4180b3a9fd996713a0cab9bae77b23686 # Parent db1c28e326fc9fd53b0c930a40ad67bc6c783928 ProofDocument without state handle text-events via actor diff -r db1c28e326fc -r aaafe9c4180b src/Tools/jEdit/src/jedit/ProverSetup.scala --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Mar 05 16:40:49 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Sun Mar 08 23:03:49 2009 +0100 @@ -9,7 +9,7 @@ import isabelle.prover.{Prover, Command} import isabelle.renderer.UserAgent - +import isabelle.proofdocument.DocumentActor import org.w3c.dom.Document @@ -39,9 +39,11 @@ val buffer = view.getBuffer val dir = buffer.getDirectory - theory_view = new TheoryView(view.getTextArea) - prover.set_document(theory_view, - if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir) + 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.activate //register output-view diff -r db1c28e326fc -r aaafe9c4180b src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Mar 05 16:40:49 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Mar 08 23:03:49 2009 +0100 @@ -8,6 +8,7 @@ package isabelle.jedit +import scala.actors.Actor import isabelle.proofdocument.Text import isabelle.prover.{Prover, Command} @@ -38,8 +39,8 @@ } -class TheoryView (text_area: JEditTextArea) - extends TextAreaExtension with Text with BufferListener { +class TheoryView (text_area: JEditTextArea, document_actor: Actor) + extends TextAreaExtension with BufferListener { private val buffer = text_area.getBuffer private val prover = Isabelle.prover_setup(buffer).get.prover @@ -88,7 +89,7 @@ text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this) buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document)) update_styles - changes.event(new Text.Change(0,buffer.getText(0, buffer.getLength),0)) + document_actor ! new Text.Change(0,buffer.getText(0, buffer.getLength),0) } def deactivate() = { @@ -185,19 +186,11 @@ gfx.setColor(saved_color) } - - /* Text methods */ - - def content(start: Int, stop: Int) = buffer.getText(start, stop - start) - def length = buffer.getLength - val changes = new EventBus[Text.Change] - - /* BufferListener methods */ private def commit { if (col != null) - changes.event(col) + document_actor ! col col = null if (col_timer.isRunning()) col_timer.stop() diff -r db1c28e326fc -r aaafe9c4180b src/Tools/jEdit/src/proofdocument/DocumentActor.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/DocumentActor.scala Sun Mar 08 23:03:49 2009 +0100 @@ -0,0 +1,35 @@ +/* + * 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 db1c28e326fc -r aaafe9c4180b src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Mar 05 16:40:49 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sun Mar 08 23:03:49 2009 +0100 @@ -2,12 +2,15 @@ * Document as list of commands, consisting of lists of tokens * * @author Johannes Hölzl, TU Munich + * @author Fabian Immler, TU Munich * @author Makarius */ package isabelle.proofdocument import scala.collection.mutable.ListBuffer +import scala.actors.Actor +import scala.actors.Actor._ import java.util.regex.Pattern import isabelle.prover.{Prover, Command} import isabelle.utils.LinearSet @@ -37,24 +40,24 @@ } -class ProofDocument(text: Text, is_command_keyword: String => Boolean) +class ProofDocument(val tokens: LinearSet[Token], + val commands: LinearSet[Command], + val active: Boolean, + is_command_keyword: String => Boolean, + structural_changes: EventBus[StructureChange]) { - private var active = false - def activate() { - if (!active) { - active = true - text_changed(new Text.Change(0, content, content.length)) - } - } - text.changes += (change => text_changed(change)) + 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 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) - var tokens = LinearSet.empty[Token] - var commands = LinearSet.empty[Command] def content = Token.string_from_tokens(List() ++ tokens) /** token view **/ - private def text_changed(change: Text.Change) + def text_changed(change: Text.Change): ProofDocument = { val tokens = List() ++ this.tokens val (begin, remaining) = tokens.span(_.stop < change.start) @@ -100,18 +103,17 @@ } } val insert = new_tokens.reverse - this.tokens = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]] + val new_tokenset = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]] token_changed(begin.lastOption, insert, removed, + new_tokenset, old_suffix.firstOption) } /** command view **/ - val structural_changes = new EventBus[StructureChange] - def find_command_at(pos: Int): Command = { for (cmd <- commands) { if (pos < cmd.stop) return cmd } return null @@ -120,7 +122,8 @@ private def token_changed(before_change: Option[Token], inserted_tokens: List[Token], removed_tokens: List[Token], - after_change: Option[Token]) + new_tokenset: LinearSet[Token], + after_change: Option[Token]): ProofDocument = { val commands = List() ++ this.commands val (begin, remaining) = @@ -164,8 +167,9 @@ val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post) System.err.println("new_commands: " + new_commands) - this.commands = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]] + 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) } } diff -r db1c28e326fc -r aaafe9c4180b src/Tools/jEdit/src/proofdocument/Text.scala --- a/src/Tools/jEdit/src/proofdocument/Text.scala Thu Mar 05 16:40:49 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/Text.scala Sun Mar 08 23:03:49 2009 +0100 @@ -11,8 +11,4 @@ case class Change(start: Int, val added: String, val removed: Int) { override def toString = "start: " + start + " added: " + added + " removed: " + removed } -} - -trait Text { - def changes: EventBus[Text.Change] -} +} \ No newline at end of file diff -r db1c28e326fc -r aaafe9c4180b src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Thu Mar 05 16:40:49 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Prover.scala Sun Mar 08 23:03:49 2009 +0100 @@ -15,7 +15,7 @@ import org.gjt.sp.util.Log import isabelle.jedit.Isabelle -import isabelle.proofdocument.{ProofDocument, Text, Token} +import isabelle.proofdocument.{DocumentActor, ProofDocument, Text, Token} import isabelle.IsarDocument @@ -81,8 +81,8 @@ val activated = new EventBus[Unit] val command_info = new EventBus[Command] val output_info = new EventBus[String] - var document: ProofDocument = null - + var document_actor: DocumentActor = null + def document = document_actor.get def command_change(c: Command) = Swing.now { command_info.event(c) } @@ -101,12 +101,7 @@ Swing.now { output_info.event(result.result) } else if (result.kind == IsabelleProcess.Kind.WRITELN && !initialized) { // FIXME !? initialized = true - Swing.now { - if (document != null) { - document.activate() - activated.event(()) - } - } + Swing.now { document_actor ! DocumentActor.Activate } } else { result.kind match { @@ -191,11 +186,16 @@ } } - def set_document(text: Text, path: String) { - this.document = new ProofDocument(text, command_decls.contains(_)) + 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)) - document.structural_changes += (changes => if(initialized){ + 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)}) })