# HG changeset patch
# User wenzelm
# Date 1282336335 -7200
# Node ID 3fa11fb01f868f018d7a6ad626131c02cda45518
# Parent  9d480f6a258934530b7f8f42ac600293b8b6d055
added Text.Range.- convenience;

diff -r 9d480f6a2589 -r 3fa11fb01f86 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Fri Aug 20 20:11:25 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Fri Aug 20 22:32:15 2010 +0200
@@ -31,6 +31,7 @@
 
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = map(_ + i)
+    def -(i: Offset): Range = map(_ - i)
     def contains(i: Offset): Boolean = start == i || start < i && i < stop
     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)