# HG changeset patch
# User wenzelm
# Date 1282132952 -7200
# Node ID f01f4ab2a0af6ff925cb3b8c3ad98860a8f8bd8c
# Parent  d72479a078822ff4a9822bfc380d643fc518da20
refined notion of Text.Range;

diff -r d72479a07882 -r f01f4ab2a0af src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Wed Aug 18 11:25:09 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Wed Aug 18 14:02:32 2010 +0200
@@ -10,15 +10,34 @@
 
 object Text
 {
-  /* offset and range */
+  /* offset */
 
   type Offset = Int
 
+
+  /* range: interval with total quasi-ordering */
+
+  object Range
+  {
+    object Ordering extends scala.math.Ordering[Range]
+    {
+      override def compare(r1: Range, r2: Range): Int = r1 compare r2
+    }
+  }
+
   sealed case class Range(val start: Offset, val stop: Offset)
   {
-    def contains(i: Offset): Boolean = start <= i && i < stop
+    require(start <= stop)
+
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = map(_ + i)
+    def contains(i: Offset): Boolean = start <= i && i < stop
+    def contains(that: Range): Boolean = start <= that.start && that.stop <= stop
+    def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
+    def compare(that: Range): Int =
+      if (overlaps(that)) 0
+      else if (this.start < that.start) -1
+      else 1
   }