src/Pure/PIDE/text.scala

     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]
+    object Ordering extends scala.math.Ordering[Range]
     {
-      def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
+      def compare(r1: Range, r2: Range): Int = r1 compare r2
     }
   }
 
   sealed case class Range(start: Offset, stop: Offset)
   {

 
     def full: Perspective = Perspective(List(Range.full))
 
     def apply(ranges: Seq[Range]): Perspective =
     {
-      val result = new mutable.ListBuffer[Text.Range]
-      var last: Option[Text.Range] = None
+      val result = new mutable.ListBuffer[Range]
+      var last: Option[Range] = None
       def ship(next: Option[Range]) { result ++= last; last = next }
 
       for (range <- ranges.sortBy(_.start))
       {
         last match {

   }
 
 
   /* information associated with text range */
 
-  sealed case class Info[A](range: Text.Range, info: A)
-  {
-    def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
-    def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
+  sealed case class Info[A](range: Range, info: A)
+  {
+    def restrict(r: Range): Info[A] = Info(range.restrict(r), info)
+    def try_restrict(r: Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
 
     def map[B](f: A => B): Info[B] = Info(range, f(info))
   }
 
   type Markup = Info[XML.Elem]

   /* text length wrt. encoding */
 
   trait Length
   {
     def apply(text: String): Int
-    def offset(text: String, i: Int): Option[Text.Offset]
+    def offset(text: String, i: Int): Option[Offset]
   }
 
   object Length extends Length
   {
     def apply(text: String): Int = text.length
-    def offset(text: String, i: Int): Option[Text.Offset] =
+    def offset(text: String, i: Int): Option[Offset] =
       if (0 <= i && i <= text.length) Some(i) else None
 
     val encodings: List[(String, Length)] =
       List(
         "UTF-16" -> Length,