src/Pure/PIDE/text.scala

   type Offset = Int
 
 
   /* range -- with total quasi-ordering */
 
+  object Range
+  {
+    def apply(start: Offset): Range = Range(start, start)
+  }
+
   sealed case class Range(val start: Offset, val stop: Offset)
   {
     // denotation: {start} Un {i. start < i & i < stop}
     require(start <= stop)
 

     def +(i: Offset): Range = map(_ + i)
     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)
 
     def restrict(that: Range): Range =
       Range(this.start max that.start, this.stop min that.stop)
   }