# HG changeset patch
# User wenzelm
# Date 1282232233 -7200
# Node ID c5eae9fc1fa41b6e1b91e40bbd3c891c9cae46c4
# Parent  9c1fde4e2487a293dcbc051715449186cfb97aba
Text.Range: improved handling of singularities;

diff -r 9c1fde4e2487 -r c5eae9fc1fa4 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Thu Aug 19 14:52:25 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Thu Aug 19 17:37:13 2010 +0200
@@ -32,12 +32,20 @@
     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 contains(that: Range): Boolean =
+      this == that || this.contains(that.start) && that.stop <= this.stop
+    def overlaps(that: Range): Boolean =
+      this == that || 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
+
+    def start_range: Range = Range(start, start)
+    def stop_range: Range = Range(stop, stop)
+
+    def intersect(that: Range): Range =
+      Range(this.start max that.start, this.stop min that.stop)
   }