src/Pure/PIDE/text.scala
changeset 57620 c30ab960875e
parent 56746 d37a5d09a277
child 57912 dd9550f84106
     1.1 --- a/src/Pure/PIDE/text.scala	Wed Jul 23 15:32:05 2014 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Wed Jul 23 16:20:07 2014 +0200
     1.3 @@ -154,8 +154,6 @@
     1.4  
     1.5      def convert(i: Offset): Offset = transform(is_insert, i)
     1.6      def revert(i: Offset): Offset = transform(!is_insert, i)
     1.7 -    def convert(range: Range): Range = range.map(convert)
     1.8 -    def revert(range: Range): Range = range.map(revert)
     1.9  
    1.10  
    1.11      /* edit strings */