diff -r 2858ec7b6dd8 -r 7066fbd315ae src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sun Aug 15 22:48:56 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Sun Aug 15 23:07:22 2010 +0200
@@ -15,6 +15,11 @@
   type Offset = Int
 
   sealed case class Range(val start: Offset, val stop: Offset)
+  {
+    def contains(i: Offset): Boolean = start <= i && i < stop
+    def map(f: Offset => Offset): Range = Range(f(start), f(stop))
+    def +(i: Offset): Range = map(_ + i)
+  }
 
 
   /* editing */