src/Pure/PIDE/text.scala
changeset 38568 f117ba49a59c
parent 38565 32b924a832c4
child 38570 3fa11fb01f86
     1.1 --- a/src/Pure/PIDE/text.scala	Fri Aug 20 11:57:43 2010 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Fri Aug 20 12:12:28 2010 +0200
     1.3 @@ -17,6 +17,11 @@
     1.4  
     1.5    /* range -- with total quasi-ordering */
     1.6  
     1.7 +  object Range
     1.8 +  {
     1.9 +    def apply(start: Offset): Range = Range(start, start)
    1.10 +  }
    1.11 +
    1.12    sealed case class Range(val start: Offset, val stop: Offset)
    1.13    {
    1.14      // denotation: {start} Un {i. start < i & i < stop}
    1.15 @@ -31,9 +36,6 @@
    1.16      def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    1.17      def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
    1.18  
    1.19 -    def start_range: Range = Range(start, start)
    1.20 -    def stop_range: Range = Range(stop, stop)
    1.21 -
    1.22      def restrict(that: Range): Range =
    1.23        Range(this.start max that.start, this.stop min that.stop)
    1.24    }