further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
authorwenzelm
Fri Aug 20 11:00:15 2010 +0200 (2010-08-20 ago)
changeset 3856532b924a832c4
parent 38564 a6e2715fac5f
child 38566 8176107637ce
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
src/Pure/General/position.scala
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/General/position.scala	Thu Aug 19 22:52:00 2010 +0200
     1.2 +++ b/src/Pure/General/position.scala	Fri Aug 20 11:00:15 2010 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4  
     1.5    def get_range(pos: T): Option[Text.Range] =
     1.6      (get_offset(pos), get_end_offset(pos)) match {
     1.7 -      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
     1.8 -      case (Some(start), None) => Some(Text.Range(start, start + 1))
     1.9 -      case (None, _) => None
    1.10 +      case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
    1.11 +      case (Some(start), None) => Some(Text.Range(start, start))
    1.12 +      case (_, _) => None
    1.13      }
    1.14  
    1.15    object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
     2.1 --- a/src/Pure/PIDE/text.scala	Thu Aug 19 22:52:00 2010 +0200
     2.2 +++ b/src/Pure/PIDE/text.scala	Fri Aug 20 11:00:15 2010 +0200
     2.3 @@ -15,25 +15,21 @@
     2.4    type Offset = Int
     2.5  
     2.6  
     2.7 -  /* range: interval with total quasi-ordering */
     2.8 +  /* range -- with total quasi-ordering */
     2.9  
    2.10    sealed case class Range(val start: Offset, val stop: Offset)
    2.11    {
    2.12 +    // denotation: {start} Un {i. start < i & i < stop}
    2.13      require(start <= stop)
    2.14  
    2.15      override def toString = "[" + start.toString + ":" + stop.toString + "]"
    2.16  
    2.17      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    2.18      def +(i: Offset): Range = map(_ + i)
    2.19 -    def contains(i: Offset): Boolean = start <= i && i < stop
    2.20 -    def contains(that: Range): Boolean =
    2.21 -      this == that || this.contains(that.start) && that.stop <= this.stop
    2.22 -    def overlaps(that: Range): Boolean =
    2.23 -      this == that || this.contains(that.start) || that.contains(this.start)
    2.24 -    def compare(that: Range): Int =
    2.25 -      if (overlaps(that)) 0
    2.26 -      else if (this.start < that.start) -1
    2.27 -      else 1
    2.28 +    def contains(i: Offset): Boolean = start == i || start < i && i < stop
    2.29 +    def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    2.30 +    def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    2.31 +    def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
    2.32  
    2.33      def start_range: Range = Range(start, start)
    2.34      def stop_range: Range = Range(stop, stop)