further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;

--- a/src/Pure/General/position.scala	Thu Aug 19 22:52:00 2010 +0200
+++ b/src/Pure/General/position.scala	Fri Aug 20 11:00:15 2010 +0200
@@ -22,9 +22,9 @@
 
   def get_range(pos: T): Option[Text.Range] =
     (get_offset(pos), get_end_offset(pos)) match {
-      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
-      case (Some(start), None) => Some(Text.Range(start, start + 1))
-      case (None, _) => None
+      case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
+      case (Some(start), None) => Some(Text.Range(start, start))
+      case (_, _) => None
     }
 
   object Id { def unapply(pos: T): Option[Long] = get_id(pos) }

--- a/src/Pure/PIDE/text.scala	Thu Aug 19 22:52:00 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Fri Aug 20 11:00:15 2010 +0200
@@ -15,25 +15,21 @@
   type Offset = Int
 
 
-  /* range: interval with total quasi-ordering */
+  /* range -- with total quasi-ordering */
 
   sealed case class Range(val start: Offset, val stop: Offset)
   {
+    // denotation: {start} Un {i. start < i & i < stop}
     require(start <= stop)
 
     override def toString = "[" + start.toString + ":" + stop.toString + "]"
 
     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 =
-      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 contains(i: Offset): Boolean = start == i || start < i && i < stop
+    def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
+    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 start_range: Range = Range(start, start)
     def stop_range: Range = Range(stop, stop)