--- 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 {
--- 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
}
--- /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
--- 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 = {
--- 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)
- }
-}
--- 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)
}
}