--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Wed Jul 08 13:29:42 2009 +0200
@@ -45,7 +45,7 @@
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), 0)
+ buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), "")
}
// register output-view
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 13:29:42 2009 +0200
@@ -116,7 +116,7 @@
val shifted =
if (start <= pos)
if (pos < start + added.length) start
- else pos - added.length + removed
+ else pos - added.length + removed.length
else pos
if (id == to_id) pos
else _from_current(to_id, rest_changes, shifted)
@@ -130,8 +130,8 @@
val shifted = _to_current(from_id, rest_changes, pos)
if (id == from_id) pos
else if (start <= shifted) {
- if (shifted < start + removed) start
- else shifted + added.length - removed
+ if (shifted < start + removed.length) start
+ else shifted + added.length - removed.length
} else shifted
}
}
@@ -259,22 +259,23 @@
{
val text = buffer.getText(offset, length)
if (col == null)
- col = new Text.Change(id(), offset, text, 0)
+ col = new Text.Change(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)
else {
commit
- col = new Text.Change(id(), offset, text, 0)
+ col = new Text.Change(id(), offset, text, "")
}
delay_commit
}
override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, start: Int, num_lines: Int, removed: Int)
+ 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(id(), start, "", removed)
- else if (col.start > start + removed || start > col.start + col.added.length) {
+ else if (col.start > start + removed_length || start > col.start + col.added.length) {
commit
col = new Text.Change(id(), start, "", removed)
}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Wed Jul 08 13:29:42 2009 +0200
@@ -57,7 +57,7 @@
new ProofDocument(id, tokens, token_start, commands, true, is_command_keyword)
def activate: (ProofDocument, StructureChange) = {
val (doc, change) =
- text_changed(new Text.Change(isabelle.jedit.Isabelle.system.id(), 0, content, content.length))
+ text_changed(new Text.Change(isabelle.jedit.Isabelle.system.id(), 0, content, content))
return (doc.mark_active, change)
}
def set_command_keyword(f: String => Boolean): ProofDocument =
@@ -74,10 +74,10 @@
// split old token lists
val tokens = Nil ++ this.tokens
val (begin, remaining) = tokens.span(stop(_) < change.start)
- val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed)
+ val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
// update indices
start = end.foldLeft(start)((s, t) =>
- s + (t -> (s(t) + change.added.length - change.removed)))
+ s + (t -> (s(t) + change.added.length - change.removed.length)))
val split_begin = removed.takeWhile(start(_) < change.start).
map (t => {
@@ -86,10 +86,10 @@
split_tok
})
- val split_end = removed.dropWhile(stop(_) < change.start + change.removed).
+ val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
map (t => {
val split_tok =
- new Token(t.content.substring(change.start + change.removed - start(t)), t.kind)
+ new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
start += (split_tok -> start(t))
split_tok
})
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Wed Jul 08 13:29:42 2009 +0200
@@ -8,7 +8,7 @@
object Text {
- case class Change(id: String, start: Int, val added: String, val removed: Int) {
+ case class Change(id: String, start: Int, val added: String, val removed: String) {
override def toString = "start: " + start + " added: " + added + " removed: " + removed
}
}
\ No newline at end of file