src/Pure/PIDE/text.scala
changeset 56308 ebd3bf053969
parent 56172 31289387fdf8
child 56468 30128d1acfbc
equal deleted inserted replaced
56307:2bdf8261677a 56308:ebd3bf053969
    43     override def toString = "[" + start.toString + ":" + stop.toString + "]"
    43     override def toString = "[" + start.toString + ":" + stop.toString + "]"
    44 
    44 
    45     def length: Int = stop - start
    45     def length: Int = stop - start
    46 
    46 
    47     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    47     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    48     def +(i: Offset): Range = map(_ + i)
    48     def +(i: Offset): Range = if (i == 0) this else map(_ + i)
    49     def -(i: Offset): Range = map(_ - i)
    49     def -(i: Offset): Range = if (i == 0) this else map(_ - i)
    50 
    50 
    51     def is_singularity: Boolean = start == stop
    51     def is_singularity: Boolean = start == stop
    52 
    52 
    53     def contains(i: Offset): Boolean = start == i || start < i && i < stop
    53     def contains(i: Offset): Boolean = start == i || start < i && i < stop
    54     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop
    54     def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop