src/Pure/PIDE/text.scala
changeset 56308 ebd3bf053969
parent 56172 31289387fdf8
child 56468 30128d1acfbc
     1.1 --- a/src/Pure/PIDE/text.scala	Thu Mar 27 20:28:19 2014 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Thu Mar 27 21:16:08 2014 +0100
     1.3 @@ -45,8 +45,8 @@
     1.4      def length: Int = stop - start
     1.5  
     1.6      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     1.7 -    def +(i: Offset): Range = map(_ + i)
     1.8 -    def -(i: Offset): Range = map(_ - i)
     1.9 +    def +(i: Offset): Range = if (i == 0) this else map(_ + i)
    1.10 +    def -(i: Offset): Range = if (i == 0) this else map(_ - i)
    1.11  
    1.12      def is_singularity: Boolean = start == stop
    1.13