src/Pure/PIDE/text.scala
changeset 64546 134ae7da2ccf
parent 64370 865b39487b5d
child 64678 914dffe59cc5
equal deleted inserted replaced
64545:25045094d7bb 64546:134ae7da2ccf
    35 
    35 
    36   sealed case class Range(start: Offset, stop: Offset)
    36   sealed case class Range(start: Offset, stop: Offset)
    37   {
    37   {
    38     // denotation: {start} Un {i. start < i & i < stop}
    38     // denotation: {start} Un {i. start < i & i < stop}
    39     if (start > stop)
    39     if (start > stop)
    40       error("Bad range: [" + start.toString + ":" + stop.toString + "]")
    40       error("Bad range: [" + start.toString + ".." + stop.toString + "]")
    41 
    41 
    42     override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
    42     override def toString: String = "[" + start.toString + ".." + stop.toString + "]"
    43 
    43 
    44     def length: Int = stop - start
    44     def length: Int = stop - start
    45 
    45 
    46     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    46     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    47     def +(i: Offset): Range = if (i == 0) this else map(_ + i)
    47     def +(i: Offset): Range = if (i == 0) this else map(_ + i)