src/Pure/PIDE/text.scala
changeset 56308 ebd3bf053969
parent 56172 31289387fdf8
child 56468 30128d1acfbc
--- 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