diff -r 2bdf8261677a -r ebd3bf053969 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