src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Wed Jul 23 15:32:05 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Wed Jul 23 16:20:07 2014 +0200
@@ -154,8 +154,6 @@
 
     def convert(i: Offset): Offset = transform(is_insert, i)
     def revert(i: Offset): Offset = transform(!is_insert, i)
-    def convert(range: Range): Range = range.map(convert)
-    def revert(range: Range): Range = range.map(revert)
 
 
     /* edit strings */