src/Pure/PIDE/text.scala
changeset 38563 f6c9a4f9f66f
parent 38562 3de5f0424caa
child 38564 a6e2715fac5f
equal deleted inserted replaced
38562:3de5f0424caa 38563:f6c9a4f9f66f
    18   /* range: interval with total quasi-ordering */
    18   /* range: interval with total quasi-ordering */
    19 
    19 
    20   sealed case class Range(val start: Offset, val stop: Offset)
    20   sealed case class Range(val start: Offset, val stop: Offset)
    21   {
    21   {
    22     require(start <= stop)
    22     require(start <= stop)
       
    23 
       
    24     override def toString = "[" + start.toString + ":" + stop.toString + "]"
    23 
    25 
    24     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    26     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    25     def +(i: Offset): Range = map(_ + i)
    27     def +(i: Offset): Range = map(_ + i)
    26     def contains(i: Offset): Boolean = start <= i && i < stop
    28     def contains(i: Offset): Boolean = start <= i && i < stop
    27     def contains(that: Range): Boolean =
    29     def contains(that: Range): Boolean =