1.1 --- a/src/Tools/jEdit/src/proofdocument/Change.scala	Thu Aug 27 10:51:09 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/Change.scala	Thu Aug 27 10:51:09 2009 +0200
     1.3 @@ -15,7 +15,8 @@
     1.4  
     1.5  case class Insert(start: Int, added: String) extends Edit {
     1.6    def from_where(x: Int) =
     1.7 -    if (start <= x && start + added.length <= x) x - added.length else x
     1.8 +    if (start > x) x
     1.9 +    else (x - added.length) max start
    1.10  
    1.11    def where_to(x: Int) =
    1.12      if (start <= x) x + added.length else x
    1.13 @@ -26,7 +27,8 @@
    1.14      if (start <= x) x + removed.length else x
    1.15  
    1.16    def where_to(x: Int) =
    1.17 -    if (start <= x && start + removed.length <= x) x - removed.length else x
    1.18 +    if (start > x) x
    1.19 +    else (x - removed.length) max start
    1.20  }
    1.21  // TODO: merge multiple inserts?
    1.22  

     2.1 --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 10:51:09 2009 +0200
     2.3 @@ -209,11 +209,15 @@
     2.4        } else Nil
     2.5  
     2.6      val split_end =
     2.7 -      if (after_change.isDefined && cmd_after_change.isDefined) {
     2.8 +      if (after_change.isDefined) {
     2.9          val unchanged = new_tokens.dropWhile(_ != after_change.get)
    2.10 -        if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
    2.11 -          unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
    2.12 -        else Nil
    2.13 +        if(cmd_after_change.isDefined) {
    2.14 +          if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
    2.15 +            unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
    2.16 +          else Nil
    2.17 +        } else {
    2.18 +          unchanged
    2.19 +        }
    2.20        } else Nil
    2.21  
    2.22      val rescan_begin =