--- 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?
--- 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 =