src/Pure/PIDE/text.scala
changeset 38570 3fa11fb01f86
parent 38568 f117ba49a59c
child 38577 4e4d3ea3725a
equal deleted inserted replaced
38569:9d480f6a2589 38570:3fa11fb01f86
    29 
    29 
    30     override def toString = "[" + start.toString + ":" + stop.toString + "]"
    30     override def toString = "[" + start.toString + ":" + stop.toString + "]"
    31 
    31 
    32     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    32     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    33     def +(i: Offset): Range = map(_ + i)
    33     def +(i: Offset): Range = map(_ + i)
       
    34     def -(i: Offset): Range = map(_ - i)
    34     def contains(i: Offset): Boolean = start == i || start < i && i < stop
    35     def contains(i: Offset): Boolean = start == i || start < i && i < stop
    35     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    36     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    36     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    37     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    37     def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
    38     def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
    38 
    39