src/Pure/PIDE/text.scala
changeset 64678 914dffe59cc5
parent 64546 134ae7da2ccf
child 64682 7e119f32276a
equal deleted inserted replaced
64677:8dc24130e8fe 64678:914dffe59cc5
    23 
    23 
    24   object Range
    24   object Range
    25   {
    25   {
    26     def apply(start: Offset): Range = Range(start, start)
    26     def apply(start: Offset): Range = Range(start, start)
    27 
    27 
       
    28     val full: Range = apply(0, Integer.MAX_VALUE / 2)
    28     val offside: Range = apply(-1)
    29     val offside: Range = apply(-1)
    29 
    30 
    30     object Ordering extends scala.math.Ordering[Text.Range]
    31     object Ordering extends scala.math.Ordering[Text.Range]
    31     {
    32     {
    32       def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    33       def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    77 
    78 
    78   object Perspective
    79   object Perspective
    79   {
    80   {
    80     val empty: Perspective = Perspective(Nil)
    81     val empty: Perspective = Perspective(Nil)
    81 
    82 
    82     def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2)))
    83     def full: Perspective = Perspective(List(Range.full))
    83 
    84 
    84     def apply(ranges: Seq[Range]): Perspective =
    85     def apply(ranges: Seq[Range]): Perspective =
    85     {
    86     {
    86       val result = new mutable.ListBuffer[Text.Range]
    87       val result = new mutable.ListBuffer[Text.Range]
    87       var last: Option[Text.Range] = None
    88       var last: Option[Text.Range] = None