# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 3f20110dfe2f412f794a3084bedaa1656c1a78bc
# Parent  a6554ba34ab2dee266947a19982b2393547c2414
fixed special case;
fixed conversion of offsets

diff -r a6554ba34ab2 -r 3f20110dfe2f src/Tools/jEdit/src/proofdocument/Change.scala
--- a/src/Tools/jEdit/src/proofdocument/Change.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Change.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -15,7 +15,8 @@
 
 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
+    if (start > x) x
+    else (x - added.length) max start
 
   def where_to(x: Int) =
     if (start <= x) x + added.length else x
@@ -26,7 +27,8 @@
     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
+    if (start > x) x
+    else (x - removed.length) max start
 }
 // TODO: merge multiple inserts?
 
diff -r a6554ba34ab2 -r 3f20110dfe2f src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -209,11 +209,15 @@
       } else Nil
 
     val split_end =
-      if (after_change.isDefined && cmd_after_change.isDefined) {
+      if (after_change.isDefined) {
         val unchanged = new_tokens.dropWhile(_ != after_change.get)
-        if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
-          unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
-        else Nil
+        if(cmd_after_change.isDefined) {
+          if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
+            unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
+          else Nil
+        } else {
+          unchanged
+        }
       } else Nil
 
     val rescan_begin =