src/Pure/PIDE/text.scala

     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
     def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
 
     def restrict(that: Range): Range =
       Range(this.start max that.start, this.stop min that.stop)
+  }
+
+
+  /* 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 */