diff -r ce3eed2b16f7 -r 4e4d3ea3725a src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -42,6 +42,15 @@
   }
 
 
+  /* information associated with text range */
+
+  case class Info[A](val range: Text.Range, val info: A)
+  {
+    def contains[B](that: Info[B]): Boolean = this.range contains that.range
+    def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
+  }
+
+
   /* editing */
 
   object Edit