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 */