1.1 --- a/src/Pure/PIDE/text.scala	Wed Aug 18 11:25:09 2010 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Wed Aug 18 14:02:32 2010 +0200
     1.3 @@ -10,15 +10,34 @@
     1.4  
     1.5  object Text
     1.6  {
     1.7 -  /* offset and range */
     1.8 +  /* offset */
     1.9  
    1.10    type Offset = Int
    1.11  
    1.12 +
    1.13 +  /* range: interval with total quasi-ordering */
    1.14 +
    1.15 +  object Range
    1.16 +  {
    1.17 +    object Ordering extends scala.math.Ordering[Range]
    1.18 +    {
    1.19 +      override def compare(r1: Range, r2: Range): Int = r1 compare r2
    1.20 +    }
    1.21 +  }
    1.22 +
    1.23    sealed case class Range(val start: Offset, val stop: Offset)
    1.24    {
    1.25 -    def contains(i: Offset): Boolean = start <= i && i < stop
    1.26 +    require(start <= stop)
    1.27 +
    1.28      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    1.29      def +(i: Offset): Range = map(_ + i)
    1.30 +    def contains(i: Offset): Boolean = start <= i && i < stop
    1.31 +    def contains(that: Range): Boolean = start <= that.start && that.stop <= stop
    1.32 +    def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    1.33 +    def compare(that: Range): Int =
    1.34 +      if (overlaps(that)) 0
    1.35 +      else if (this.start < that.start) -1
    1.36 +      else 1
    1.37    }
    1.38  
    1.39