tuned;
authorwenzelm
Thu, 27 Mar 2014 21:16:08 +0100
changeset 56308 ebd3bf053969
parent 56307 2bdf8261677a
child 56309 5003ea266aef
tuned;
src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Thu Mar 27 20:28:19 2014 +0100
+++ b/src/Pure/PIDE/text.scala	Thu Mar 27 21:16:08 2014 +0100
@@ -45,8 +45,8 @@
     def length: Int = stop - start
 
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
-    def +(i: Offset): Range = map(_ + i)
-    def -(i: Offset): Range = map(_ - i)
+    def +(i: Offset): Range = if (i == 0) this else map(_ + i)
+    def -(i: Offset): Range = if (i == 0) this else map(_ - i)
 
     def is_singularity: Boolean = start == stop