# HG changeset patch
# User immler@in.tum.de
# Date 1247052582 -7200
# Node ID 8213a350fd452f02b338c5d41c17d4c28a5f66c0
# Parent  2b8d2acfda4eeaf92501825bebb9eb0eca6da4ef
remember removed text

diff -r 2b8d2acfda4e -r 8213a350fd45 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- 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
diff -r 2b8d2acfda4e -r 8213a350fd45 src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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)
     }
diff -r 2b8d2acfda4e -r 8213a350fd45 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- 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
         })
diff -r 2b8d2acfda4e -r 8213a350fd45 src/Tools/jEdit/src/proofdocument/Text.scala
--- 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