# HG changeset patch
# User wenzelm
# Date 1482920911 -3600
# Node ID 914dffe59cc5d237e63ce64f72cf037ab20d12e5
# Parent  8dc24130e8fe41084bbb619d6539f9e9184a1860
tuned;

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 =
     {