# HG changeset patch
# User wenzelm
# Date 1281025079 -7200
# Node ID 343cb5d4034aeaa375657c1c55d9638a25ec3f06
# Parent  469555615ec70a914440c01dca487696e0b7f72b
Text_Edit.convert/revert;

diff -r 469555615ec7 -r 343cb5d4034a src/Pure/PIDE/change.scala
--- a/src/Pure/PIDE/change.scala	Thu Aug 05 18:13:12 2010 +0200
+++ b/src/Pure/PIDE/change.scala	Thu Aug 05 18:17:59 2010 +0200
@@ -74,8 +74,8 @@
       val document = stable.join_document
       val node = document.nodes(name)
       val is_outdated = !(extra_edits.isEmpty && latest == stable)
-      def convert(offset: Int): Int = (offset /: changes)((i, change) => change after i)
-      def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change before i)  // FIXME fold_rev (!?)
+      def convert(offset: Int): Int = (offset /: changes)((i, change) => change.convert(i))
+      def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change.revert(i))  // FIXME fold_rev (!?)
     }
   }
 }
\ No newline at end of file
diff -r 469555615ec7 -r 343cb5d4034a src/Pure/PIDE/text_edit.scala
--- a/src/Pure/PIDE/text_edit.scala	Thu Aug 05 18:13:12 2010 +0200
+++ b/src/Pure/PIDE/text_edit.scala	Thu Aug 05 18:17:59 2010 +0200
@@ -21,8 +21,8 @@
     else if (is_insert == do_insert) offset + text.length
     else (offset - text.length) max start
 
-  def after(offset: Int): Int = transform(true, offset)
-  def before(offset: Int): Int = transform(false, offset)
+  def convert(offset: Int): Int = transform(true, offset)
+  def revert(offset: Int): Int = transform(false, offset)
 
 
   /* edit strings */