1.1 --- a/src/Pure/PIDE/text.scala	Thu Aug 19 14:52:25 2010 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Thu Aug 19 17:37:13 2010 +0200
     1.3 @@ -32,12 +32,20 @@
     1.4      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     1.5      def +(i: Offset): Range = map(_ + i)
     1.6      def contains(i: Offset): Boolean = start <= i && i < stop
     1.7 -    def contains(that: Range): Boolean = start <= that.start && that.stop <= stop
     1.8 -    def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
     1.9 +    def contains(that: Range): Boolean =
    1.10 +      this == that || this.contains(that.start) && that.stop <= this.stop
    1.11 +    def overlaps(that: Range): Boolean =
    1.12 +      this == that || this.contains(that.start) || that.contains(this.start)
    1.13      def compare(that: Range): Int =
    1.14        if (overlaps(that)) 0
    1.15        else if (this.start < that.start) -1
    1.16        else 1
    1.17 +
    1.18 +    def start_range: Range = Range(start, start)
    1.19 +    def stop_range: Range = Range(stop, stop)
    1.20 +
    1.21 +    def intersect(that: Range): Range =
    1.22 +      Range(this.start max that.start, this.stop min that.stop)
    1.23    }
    1.24  
    1.25