# HG changeset patch # User immler@in.tum.de # Date 1247052584 -7200 # Node ID d7ba607bf684a46aa5118eef9bdeae9a44eca6e6 # Parent 70759ca6bb87c7fa61e530a56ee834199921b44e current version in theoryview/buffer diff -r 70759ca6bb87 -r d7ba607bf684 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 13:29:43 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 13:29:44 2009 +0200 @@ -106,14 +106,13 @@ val start = buffer.getLineStartOffset(line) val stop = start + line_segment.count - val document = prover.document val theory_view = Isabelle.prover_setup(buffer).get.theory_view + val document = theory_view.current_document() def to: Int => Int = theory_view.to_current(document.id, _) def from: Int => Int = theory_view.from_current(document.id, _) + var command = document.find_command_at(from(start)) var next_x = start - - var command = document.find_command_at(from(start)) while (command != null && command.start(document) < from(stop)) { for { markup <- command.highlight_node.flatten diff -r 70759ca6bb87 -r d7ba607bf684 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala --- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Wed Jul 08 13:29:43 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Wed Jul 08 13:29:44 2009 +0200 @@ -48,8 +48,8 @@ if (!prover.isDefined || !theory_view_opt.isDefined) null else if (prover.get == null || theory_view_opt.get == null) null else { - val document = prover.get.document val theory_view = theory_view_opt.get + val document = theory_view.current_document() val offset = theory_view.from_current(document, original_offset) val cmd = document.find_command_at(offset) if (cmd != null) { diff -r 70759ca6bb87 -r d7ba607bf684 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Wed Jul 08 13:29:43 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Wed Jul 08 13:29:44 2009 +0200 @@ -32,7 +32,7 @@ val prover_setup = Isabelle.plugin.prover_setup(buffer) if (prover_setup.isDefined) { - val document = prover_setup.get.prover.document + val document = prover_setup.get.theory_view.current_document() for (command <- document.commands) data.root.add(command.markup_root.swing_node(document)) diff -r 70759ca6bb87 -r d7ba607bf684 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Jul 08 13:29:43 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Jul 08 13:29:44 2009 +0200 @@ -79,9 +79,9 @@ override def paintComponent(gfx : Graphics) { super.paintComponent(gfx) - val buffer = textarea.getBuffer - val document = prover.document + val theory_view = Isabelle.prover_setup(buffer).get.theory_view + val document = theory_view.current_document() for (c <- document.commands) paintCommand(c, buffer, document, gfx) diff -r 70759ca6bb87 -r d7ba607bf684 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:43 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:44 2009 +0200 @@ -54,6 +54,8 @@ private var col: Text.Change = null + private var doc_id: IsarDocument.Document_ID = prover.document(null).id + def current_document() = prover.document(doc_id) private val col_timer = new Timer(300, new ActionListener() { override def actionPerformed(e: ActionEvent) = commit @@ -70,7 +72,7 @@ private val selected_state_controller = new CaretListener { override def caretUpdate(e: CaretEvent) = { - val doc = prover.document + val doc = current_document() val cmd = doc.find_command_at(e.getDot) if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot && Isabelle.prover_setup(buffer).get.selected_state != cmd) @@ -85,12 +87,9 @@ buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) buffer.addBufferListener(this) - val MAX = TheoryView.MAX_CHANGE_LENGTH - for (i <- 0 to buffer.getLength / MAX) { - prover ! new isabelle.proofdocument.Text.Change( - Isabelle.system.id(), i * MAX, - buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), "") - } + col = Text.Change(doc_id, Isabelle.system.id(), 0, + buffer.getText(0, buffer.getLength), "") + commit } def deactivate() { @@ -124,7 +123,7 @@ def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int = changes match { case Nil => pos - case Text.Change(id, start, added, removed) :: rest_changes => { + case Text.Change(_, id, start, added, removed) :: rest_changes => { val shifted = if (start <= pos) if (pos < start + added.length) start @@ -138,7 +137,7 @@ def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int = changes match { case Nil => pos - case Text.Change(id, start, added, removed) :: rest_changes => { + case Text.Change(_, id, start, added, removed) :: rest_changes => { val shifted = _to_current(from_id, rest_changes, pos) if (id == from_id) pos else if (start <= shifted) { @@ -159,7 +158,7 @@ def repaint(cmd: Command) = { - val document = prover.document + val document = current_document() if (text_area != null) { val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document))) val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1) @@ -202,7 +201,7 @@ override def paintValidLine(gfx: Graphics2D, screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) { - val document = prover.document + val document = current_document() def from_current(pos: Int) = this.from_current(document.id, pos) def to_current(pos: Int) = this.to_current(document.id, pos) val saved_color = gfx.getColor @@ -222,7 +221,7 @@ } override def getToolTipText(x: Int, y: Int) = { - val document = prover.document + val document = current_document() val offset = from_current(document.id, text_area.xyToOffset(x, y)) val cmd = document.find_command_at(offset) if (cmd != null) { @@ -240,12 +239,13 @@ def split_changes(c: Text.Change): List[Text.Change] = { val MAX = TheoryView.MAX_CHANGE_LENGTH if (c.added.length <= MAX) List(c) - else Text.Change(c.id, c.start, c.added.substring(0, MAX), c.removed) :: - split_changes(new Text.Change(id(), c.start + MAX, c.added.substring(MAX), c.removed)) + else Text.Change(c.base_id, c.id, c.start, c.added.substring(0, MAX), c.removed) :: + split_changes(new Text.Change(c.id, id(), c.start + MAX, c.added.substring(MAX), "")) } val new_changes = split_changes(col) changes = new_changes.reverse ::: changes new_changes map (document_actor ! _) + doc_id = new_changes.last.id } col = null if (col_timer.isRunning()) @@ -271,12 +271,12 @@ { val text = buffer.getText(offset, length) if (col == null) - col = new Text.Change(id(), offset, text, "") + col = new Text.Change(doc_id, id(), offset, text, "") else if (col.start <= offset && offset <= col.start + col.added.length) - col = new Text.Change(col.id, col.start, col.added + text, col.removed) + col = new Text.Change(doc_id, col.id, col.start, col.added + text, col.removed) else { commit - col = new Text.Change(id(), offset, text, "") + col = new Text.Change(doc_id, id(), offset, text, "") } delay_commit } @@ -286,10 +286,10 @@ { val removed = buffer.getText(start, removed_length) if (col == null) - col = new Text.Change(id(), start, "", removed) + col = new Text.Change(doc_id, id(), start, "", removed) else if (col.start > start + removed_length || start > col.start + col.added.length) { commit - col = new Text.Change(id(), start, "", removed) + col = new Text.Change(doc_id, id(), start, "", removed) } else { /* val offset = start - col.start @@ -301,7 +301,7 @@ (diff - (offset min 0), offset min 0) col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/ commit - col = new Text.Change(id(), start, "", removed) + col = new Text.Change(doc_id, id(), start, "", removed) } delay_commit } diff -r 70759ca6bb87 -r d7ba607bf684 src/Tools/jEdit/src/proofdocument/Text.scala --- a/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 13:29:43 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 13:29:44 2009 +0200 @@ -8,7 +8,12 @@ object Text { - case class Change(id: String, start: Int, val added: String, val removed: String) { + case class Change( + base_id: String, + id: String, + start: Int, + added: String, + removed: String) { override def toString = "start: " + start + " added: " + added + " removed: " + removed } } \ No newline at end of file diff -r 70759ca6bb87 -r d7ba607bf684 src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 13:29:43 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 13:29:44 2009 +0200 @@ -23,8 +23,6 @@ object ProverEvents { case class Activate - case class SetEventBus(bus: EventBus[StructureChange]) - case class SetIsCommandKeyword(is_command_keyword: String => Boolean) } class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor @@ -47,12 +45,13 @@ mutable.SynchronizedMap[IsarDocument.State_ID, Command] private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with mutable.SynchronizedMap[IsarDocument.Command_ID, Command] - private var document_versions = - List(ProofDocument.empty.set_command_keyword(command_decls.contains)) - private val document_id0 = ProofDocument.empty.id + private val document_0 = + ProofDocument.empty.set_command_keyword(command_decls.contains) + private var document_versions = List(document_0) def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id) - def document = document_versions.head + def document(id: IsarDocument.Document_ID) = + document_versions.find(_.id == id).getOrElse(document_0) private var initialized = false @@ -91,7 +90,7 @@ private def handle_result(result: Isabelle_Process.Result) { - def command_change(c: Command) = this ! c + def command_change(c: Command) = change_receiver ! c val (running, command) = result.props.find(p => p._1 == Markup.ID) match { case None => (false, null) @@ -231,38 +230,34 @@ loop { react { case change: Text.Change => { - val old = document + val old = document(change.base_id) val (doc, structure_change) = old.text_changed(change) document_versions ::= doc - edit_document(old.id, doc.id, structure_change) + edit_document(old, doc, structure_change) } - case command: Command => { - //state of command has changed - change_receiver ! command - } + case x => System.err.println("warning: ignored " + x) } } } def set_document(change_receiver: Actor, path: String) { this.change_receiver = change_receiver - process.begin_document(document_id0, path) + process.begin_document(document_0.id, path) } - private def edit_document(old_id: String, document_id: String, changes: StructureChange) = - Swing_Thread.now { - val removes = - for (cmd <- changes.removed_commands) yield { - commands -= cmd.id - if (cmd.state_id != null) states -= cmd.state_id - changes.before_change.map(_.id).getOrElse(document_id0) -> 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(document_id0)) -> Some(cmd.id) - } - process.edit_document(old_id, document_id, removes.reverse ++ inserts) - } + private def edit_document(old: ProofDocument, doc: ProofDocument, changes: StructureChange) = { + val removes = + for (cmd <- changes.removed_commands) yield { + commands -= cmd.id + if (cmd.state_id != null) states -= cmd.state_id + changes.before_change.map(_.id).getOrElse(document_0.id) -> None + } + val inserts = + for (cmd <- changes.added_commands) yield { + commands += (cmd.id -> cmd) + process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) + (doc.commands.prev(cmd).map(_.id).getOrElse(document_0.id)) -> Some(cmd.id) + } + process.edit_document(old.id, doc.id, removes.reverse ++ inserts) + } }