# HG changeset patch # User immler@in.tum.de # Date 1249643099 -7200 # Node ID e0561943bfc974ce0c253b3c664fd08b737fb49c # Parent e888d0cdda9c3ff2a500503d94d1fedb61067bd9 Change consisting of a list of Edits diff -r e888d0cdda9c -r e0561943bfc9 src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala --- a/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Mon Aug 03 16:56:33 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Fri Aug 07 13:04:59 2009 +0200 @@ -6,7 +6,7 @@ package isabelle.jedit -import isabelle.proofdocument.Text +import isabelle.proofdocument.Change import java.awt.Dimension import scala.swing.{ListView, FlowPanel} @@ -21,7 +21,7 @@ if (position == DockableWindowManager.FLOATING) preferredSize = new Dimension(500, 250) - val list = new ListView[Text.Change] + val list = new ListView[Change] list.fixedCellWidth = 500 new javax.swing.Timer(1000, new java.awt.event.ActionListener { diff -r e888d0cdda9c -r e0561943bfc9 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Aug 03 16:56:33 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Fri Aug 07 13:04:59 2009 +0200 @@ -11,7 +11,7 @@ import scala.actors.Actor import scala.actors.Actor._ -import isabelle.proofdocument.{ProofDocument, Text} +import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove} import isabelle.prover.{Prover, ProverEvents, Command} import java.awt.Graphics2D @@ -27,8 +27,6 @@ object TheoryView { - - val MAX_CHANGE_LENGTH = 1500 def choose_color(cmd: Command, doc: ProofDocument): Color = { cmd.status(doc) match { @@ -51,7 +49,7 @@ private val prover = Isabelle.prover_setup(buffer).get.prover - private var col: Text.Change = null + private var edits: List[Edit] = Nil private val col_timer = new Timer(300, new ActionListener() { override def actionPerformed(e: ActionEvent) = commit }) @@ -82,8 +80,7 @@ buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) buffer.addBufferListener(this) - col = Text.Change(Some(current_change), Isabelle.system.id(), 0, - buffer.getText(0, buffer.getLength), "") + edits = List(Insert(0, buffer.getText(0, buffer.getLength))) commit } @@ -116,37 +113,14 @@ } - def transform_back(from: Text.Change, to: Text.Change, pos: Int): Int = - if (from.id == to.id) pos - else { - val shifted = - if (from.start <= pos) - if (pos < from.start + from.added.length) from.start - else pos - from.added.length + from.removed.length - else pos - transform_back(from.base.get, to, shifted) - } + def changes_to(doc: ProofDocument) = + edits ::: current_change.ancestors(_.id == doc.id).flatten(_.toList) - def transform_forward(from: Text.Change, to: Text.Change, pos: Int): Int = - if (from.id == to.id) pos - else { - val shifted = transform_forward(from, to.base.get, pos) - if (to.start <= shifted) { - if (shifted < to.start + to.removed.length) to.start - else shifted + to.added.length - to.removed.length - } else shifted - } - - def from_current(doc: ProofDocument, pos: Int) = { - val from = if (col == null) current_change else col - val to = changes.find(_.id == doc.id).get - transform_back(from, to, pos) - } - def to_current(doc: ProofDocument, pos: Int) = { - val from = changes.find(_.id == doc.id).get - val to = if (col == null) current_change else col - transform_forward(from, to, pos) - } + def from_current(doc: ProofDocument, pos: Int) = + (pos /: changes_to(doc)) ((p, c) => c from_where p) + + def to_current(doc: ProofDocument, pos: Int) = + (pos /: changes_to(doc).reverse) ((p, c) => c where_to p) def repaint(cmd: Command) = { @@ -225,27 +199,30 @@ /* history of changes - TODO: seperate class?*/ - val change_0 = Text.Change(None, prover.document_0.id, 0, "", "") + val change_0 = new Change(prover.document_0.id, None, Nil) private var changes = List(change_0) private var current_change = change_0 def get_changes = changes - - private def doc_or_pred(c: Text.Change): ProofDocument = - prover.document(c.id).getOrElse(doc_or_pred(c.base.get)) + + private def doc_or_pred(c: Change): ProofDocument = + prover.document(c.id).getOrElse(doc_or_pred(c.parent.get)) def current_document() = doc_or_pred(current_change) /* update to desired version */ - def set_version(goal: Text.Change) { + def set_version(goal: Change) { // changes in buffer must be ignored buffer.removeBufferListener(this) - def apply(c: Text.Change) = { - buffer.remove(c.start, c.removed.length) - buffer.insert(c.start, c.added)} - def unapply(c: Text.Change) = { - buffer.remove(c.start, c.added.length) - buffer.insert(c.start, c.removed)} + def apply(c: Change) = c.map { + case Insert(start, added) => buffer.insert(start, added) + case Remove(start, removed) => buffer.remove(start, removed.length) + } + + def unapply(c: Change) = c.map { + case Insert(start, added) => buffer.remove(start, added.length) + case Remove(start, removed) => buffer.insert(start, removed) + } // undo/redo changes val ancs_current = current_change.ancestors @@ -283,19 +260,13 @@ /* BufferListener methods */ private def commit: Unit = synchronized { - if (col != null) { - 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.base, c.id, c.start, c.added.substring(0, MAX), c.removed) :: - split_changes(Text.Change(Some(c), id(), c.start + MAX, c.added.substring(MAX), "")) - } - val new_changes = split_changes(col) - changes ++= new_changes - new_changes map (document_actor ! _) - current_change = new_changes.last + if (!edits.isEmpty) { + val change = new Change(Isabelle.system.id(), Some(current_change), edits) + changes ::= change + document_actor ! change + current_change = change } - col = null + edits = Nil if (col_timer.isRunning()) col_timer.stop() } @@ -317,41 +288,14 @@ override def preContentInserted(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, length: Int) { - val text = buffer.getText(offset, length) - if (col == null) - col = new Text.Change(Some(current_change), id(), offset, text, "") - else if (col.start <= offset && offset <= col.start + col.added.length) - col = new Text.Change(Some(current_change), col.id, - col.start, col.added + text, col.removed) - else { - commit - col = new Text.Change(Some(current_change), id(), offset, text, "") - } + edits ::= Insert(offset, buffer.getText(offset, length)) delay_commit } override def preContentRemoved(buffer: JEditBuffer, start_line: Int, start: Int, num_lines: Int, removed_length: Int) { - val removed = buffer.getText(start, removed_length) - if (col == null) - col = new Text.Change(Some(current_change), id(), start, "", removed) - else if (col.start > start + removed_length || start > col.start + col.added.length) { - commit - col = new Text.Change(Some(current_change), id(), start, "", removed) - } - else { -/* val offset = start - col.start - val diff = col.added.length - removed - val (added, add_removed) = - if (diff < offset) - (offset max 0, diff - (offset max 0)) - else - (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(Some(current_change), id(), start, "", removed) - } + edits ::= Remove(start, buffer.getText(start, removed_length)) delay_commit } diff -r e888d0cdda9c -r e0561943bfc9 src/Tools/jEdit/src/proofdocument/Change.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/Change.scala Fri Aug 07 13:04:59 2009 +0200 @@ -0,0 +1,47 @@ +/* + * Changes in text + * + * @author Johannes Hölzl, TU Munich + * @author Fabian Immler, TU Munich + */ + +package isabelle.proofdocument + +abstract class Edit { + val start: Int + def from_where (x: Int): Int //where has x been before applying this edit + def where_to(x: Int): Int //where will x be when we apply this edit +} + +case class Insert(start: Int, added: String) extends Edit { + def from_where(x: Int) = + if (start <= x && start + added.length <= x) x - added.length else x + + def where_to(x: Int) = + if (start <= x) x + added.length else x +} + +case class Remove(start: Int, removed: String) extends Edit { + def from_where(x: Int) = + if (start <= x) x + removed.length else x + + def where_to(x: Int) = + if (start <= x && start + removed.length <= x) x - removed.length else x +} +// TODO: merge multiple inserts? + +class Change( + val id: String, + val parent: Option[Change], + edits: List[Edit]) extends Iterable[Edit] +{ + override def elements = edits.reverse.elements + + def ancestors(root_p: Change => Boolean): List[Change] = + if (root_p(this)) Nil + else this :: parent.map(_.ancestors(root_p)).getOrElse(Nil) + def ancestors: List[Change] = ancestors(_ => false) + + override def toString = + "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")" +} \ No newline at end of file diff -r e888d0cdda9c -r e0561943bfc9 src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Aug 03 16:56:33 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Fri Aug 07 13:04:59 2009 +0200 @@ -13,10 +13,6 @@ import isabelle.prover.{Prover, Command} import isabelle.utils.LinearSet -case class StructureChange( - val before_change: Option[Command], - val added_commands: List[Command], - val removed_commands: List[Command]) object ProofDocument { @@ -36,9 +32,11 @@ "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" + "[()\\[\\]{}:;]", Pattern.MULTILINE) - val empty = - new ProofDocument(isabelle.jedit.Isabelle.system.id(), - LinearSet(), Map(), LinearSet(), Map(), _ => false) + val empty = + new ProofDocument(isabelle.jedit.Isabelle.system.id(), + LinearSet(), Map(), LinearSet(), Map(), _ => false) + + type StructureChange = List[(Option[Command], Option[Command])] } @@ -50,7 +48,7 @@ var states: Map[Command, IsarDocument.State_ID], is_command_keyword: String => Boolean) { - + import ProofDocument.StructureChange def set_command_keyword(f: String => Boolean): ProofDocument = new ProofDocument(id, tokens, token_start, commands, states, f) @@ -60,8 +58,24 @@ /** token view **/ - def text_changed(change: Text.Change): (ProofDocument, StructureChange) = + def text_changed(c: Change): (ProofDocument, StructureChange) = { + def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = { + val (doc, chgs) = doc_chgs + val (new_doc, chg) = doc.text_edit(edit, c.id) + (new_doc, chgs ++ chg) + } + ((this, Nil: StructureChange) /: c) (edit_doc) + } + + def text_edit(e: Edit, id: String): + (ProofDocument,StructureChange) = + { + case class TextChange(start: Int, added: String, removed: String) + val change = e match { + case Insert(s, a) => TextChange(s, a, "") + case Remove(s, r) => TextChange(s, "", r) + } //indices of tokens var start: Map[Token, Int] = token_start def stop(t: Token) = start(t) + t.length @@ -115,7 +129,7 @@ start += (new_token -> (match_start + matcher.start)) new_tokens ::= new_token - invalid_tokens = invalid_tokens dropWhile (stop(_) <= stop(new_token)) + invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token)) invalid_tokens match { case t :: ts => if (start(t) == start(new_token) && @@ -129,7 +143,7 @@ } val insert = new_tokens.reverse val new_token_list = begin ::: insert ::: old_suffix - token_changed(change.id, begin.lastOption, insert, + token_changed(id, begin.lastOption, insert, old_suffix.firstOption, new_token_list, start) } @@ -142,7 +156,8 @@ inserted_tokens: List[Token], after_change: Option[Token], new_tokens: List[Token], - new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) = + new_token_start: Map[Token, Int]): + (ProofDocument, StructureChange) = { val new_tokenset = (LinearSet() ++ new_tokens).asInstanceOf[LinearSet[Token]] val cmd_before_change = before_change match { @@ -209,7 +224,6 @@ split_end val inserted_commands = tokens_to_commands(rescanning_tokens.toList) - val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList) // build new document val new_commandset = commands.delete_between(cmd_before_change, cmd_after_change). insert_after(cmd_before_change, inserted_commands) @@ -217,7 +231,13 @@ val doc = new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, states -- removed_commands, is_command_keyword) - return (doc, change) + + val removes = + for (cmd <- removed_commands) yield (cmd_before_change -> None) + val inserts = + for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd)) + + return (doc, removes.toList ++ inserts) } val commands_offsets = { diff -r e888d0cdda9c -r e0561943bfc9 src/Tools/jEdit/src/proofdocument/Text.scala --- a/src/Tools/jEdit/src/proofdocument/Text.scala Mon Aug 03 16:56:33 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -/* - * Changes in text as event - * - * @author Johannes Hölzl, TU Munich - */ - -package isabelle.proofdocument - - -object Text { - case class Change( - base: Option[Change], - id: String, - start: Int, - added: String, - removed: String) - { - override def toString = id + ": added '" + added + "'; removed '" + removed + "'" - - def ancestors: List[Text.Change] = - this :: base.map(_.ancestors).getOrElse(Nil) - } -} diff -r e888d0cdda9c -r e0561943bfc9 src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Mon Aug 03 16:56:33 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Fri Aug 07 13:04:59 2009 +0200 @@ -18,7 +18,7 @@ import org.gjt.sp.util.Log import isabelle.jedit.Isabelle -import isabelle.proofdocument.{StructureChange, ProofDocument, Text, Token} +import isabelle.proofdocument.{ProofDocument, Change, Token} import isabelle.IsarDocument object ProverEvents { @@ -228,8 +228,8 @@ import ProverEvents._ loop { react { - case change: Text.Change => { - val old = document(change.base.get.id).get + case change: Change => { + val old = document(change.parent.get.id).get val (doc, structure_change) = old.text_changed(change) document_versions ::= doc edit_document(old, doc, structure_change) @@ -244,18 +244,18 @@ process.begin_document(document_0.id, path) } - private def edit_document(old: ProofDocument, doc: ProofDocument, changes: StructureChange) = { - val removes = - for (cmd <- changes.removed_commands) yield { - commands -= cmd.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) + private def edit_document(old: ProofDocument, doc: ProofDocument, + changes: ProofDocument.StructureChange) = { + val id_changes = changes map {case (c1, c2) => + (c1.map(_.id).getOrElse(document_0.id), + c2 match { + case None => None + case Some(cmd) => + commands += (cmd.id -> cmd) + process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) + Some(cmd.id) + }) + } + process.edit_document(old.id, doc.id, id_changes) } }