src/Pure/PIDE/text.scala
changeset 38725 3d9d5ff80f6f
parent 38662 4d4553e09337
child 43425 0a5612040a8b
equal deleted inserted replaced
38724:d1feec02cf02 38725:3d9d5ff80f6f
    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 -(i: Offset): Range = map(_ - i)
    35 
    35 
    36     def is_singleton: Boolean = start == stop
    36     def is_singularity: Boolean = start == stop
    37 
    37 
    38     def contains(i: Offset): Boolean = start == i || start < i && i < stop
    38     def contains(i: Offset): Boolean = start == i || start < i && i < stop
    39     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    39     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    40     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    40     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    41     def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
    41     def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start