src/Pure/PIDE/line.scala
changeset 64647 bbfcef118acb
parent 64619 e3d9a31281f3
child 64649 d67c3094a0c2
equal deleted inserted replaced
64646:805c5e6fa430 64647:bbfcef118acb
    42   }
    42   }
    43 
    43 
    44 
    44 
    45   /* range (right-open interval) */
    45   /* range (right-open interval) */
    46 
    46 
       
    47   object Range
       
    48   {
       
    49     val zero: Range = Range(Position.zero, Position.zero)
       
    50   }
       
    51 
    47   sealed case class Range(start: Position, stop: Position)
    52   sealed case class Range(start: Position, stop: Position)
    48   {
    53   {
    49     if (start.compare(stop) > 0)
    54     if (start.compare(stop) > 0)
    50       error("Bad line range: " + start.print + ".." + stop.print)
    55       error("Bad line range: " + start.print + ".." + stop.print)
    51 
    56 
    52     def print: String = start.print + ".." + stop.print
    57     def print: String =
       
    58       if (start == stop) start.print
       
    59       else start.print + ".." + stop.print
    53   }
    60   }
    54 
    61 
    55 
    62 
    56   /* document with newline as separator (not terminator) */
    63   /* document with newline as separator (not terminator) */
    57 
    64