1.1 --- a/src/Pure/PIDE/change.scala	Thu Aug 05 18:13:12 2010 +0200
     1.2 +++ b/src/Pure/PIDE/change.scala	Thu Aug 05 18:17:59 2010 +0200
     1.3 @@ -74,8 +74,8 @@
     1.4        val document = stable.join_document
     1.5        val node = document.nodes(name)
     1.6        val is_outdated = !(extra_edits.isEmpty && latest == stable)
     1.7 -      def convert(offset: Int): Int = (offset /: changes)((i, change) => change after i)
     1.8 -      def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change before i)  // FIXME fold_rev (!?)
     1.9 +      def convert(offset: Int): Int = (offset /: changes)((i, change) => change.convert(i))
    1.10 +      def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change.revert(i))  // FIXME fold_rev (!?)
    1.11      }
    1.12    }
    1.13  }
    1.14 \ No newline at end of file

     2.1 --- a/src/Pure/PIDE/text_edit.scala	Thu Aug 05 18:13:12 2010 +0200
     2.2 +++ b/src/Pure/PIDE/text_edit.scala	Thu Aug 05 18:17:59 2010 +0200
     2.3 @@ -21,8 +21,8 @@
     2.4      else if (is_insert == do_insert) offset + text.length
     2.5      else (offset - text.length) max start
     2.6  
     2.7 -  def after(offset: Int): Int = transform(true, offset)
     2.8 -  def before(offset: Int): Int = transform(false, offset)
     2.9 +  def convert(offset: Int): Int = transform(true, offset)
    2.10 +  def revert(offset: Int): Int = transform(false, offset)
    2.11  
    2.12  
    2.13    /* edit strings */