tuned;
authorwenzelm
Thu Mar 27 21:16:08 2014 +0100 (2014-03-27)
changeset 56308ebd3bf053969
parent 56307 2bdf8261677a
child 56309 5003ea266aef
tuned;
src/Pure/PIDE/text.scala
     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