src/Pure/PIDE/text.scala
changeset 64678 914dffe59cc5
parent 64546 134ae7da2ccf
child 64682 7e119f32276a
     1.1 --- a/src/Pure/PIDE/text.scala	Wed Dec 28 10:39:50 2016 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Wed Dec 28 11:28:31 2016 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4    {
     1.5      def apply(start: Offset): Range = Range(start, start)
     1.6  
     1.7 +    val full: Range = apply(0, Integer.MAX_VALUE / 2)
     1.8      val offside: Range = apply(-1)
     1.9  
    1.10      object Ordering extends scala.math.Ordering[Text.Range]
    1.11 @@ -79,7 +80,7 @@
    1.12    {
    1.13      val empty: Perspective = Perspective(Nil)
    1.14  
    1.15 -    def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2)))
    1.16 +    def full: Perspective = Perspective(List(Range.full))
    1.17  
    1.18      def apply(ranges: Seq[Range]): Perspective =
    1.19      {