diff -r 8dc24130e8fe -r 914dffe59cc5 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Wed Dec 28 10:39:50 2016 +0100 +++ b/src/Pure/PIDE/text.scala Wed Dec 28 11:28:31 2016 +0100 @@ -25,6 +25,7 @@ { def apply(start: Offset): Range = Range(start, start) + val full: Range = apply(0, Integer.MAX_VALUE / 2) val offside: Range = apply(-1) object Ordering extends scala.math.Ordering[Text.Range] @@ -79,7 +80,7 @@ { val empty: Perspective = Perspective(Nil) - def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2))) + def full: Perspective = Perspective(List(Range.full)) def apply(ranges: Seq[Range]): Perspective = {