tuned;
authorwenzelm
Wed Mar 08 20:25:57 2017 +0100 (2017-03-08 ago)
changeset 65154ba1929b749f0
parent 65153 82bd5d29adbf
child 65155 25bccf5bf33e
tuned;
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/PIDE/text.scala	Wed Mar 08 11:45:41 2017 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Wed Mar 08 20:25:57 2017 +0100
     1.3 @@ -28,9 +28,9 @@
     1.4      val full: Range = apply(0, Integer.MAX_VALUE / 2)
     1.5      val offside: Range = apply(-1)
     1.6  
     1.7 -    object Ordering extends scala.math.Ordering[Text.Range]
     1.8 +    object Ordering extends scala.math.Ordering[Range]
     1.9      {
    1.10 -      def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    1.11 +      def compare(r1: Range, r2: Range): Int = r1 compare r2
    1.12      }
    1.13    }
    1.14  
    1.15 @@ -84,8 +84,8 @@
    1.16  
    1.17      def apply(ranges: Seq[Range]): Perspective =
    1.18      {
    1.19 -      val result = new mutable.ListBuffer[Text.Range]
    1.20 -      var last: Option[Text.Range] = None
    1.21 +      val result = new mutable.ListBuffer[Range]
    1.22 +      var last: Option[Range] = None
    1.23        def ship(next: Option[Range]) { result ++= last; last = next }
    1.24  
    1.25        for (range <- ranges.sortBy(_.start))
    1.26 @@ -124,10 +124,10 @@
    1.27  
    1.28    /* information associated with text range */
    1.29  
    1.30 -  sealed case class Info[A](range: Text.Range, info: A)
    1.31 +  sealed case class Info[A](range: Range, info: A)
    1.32    {
    1.33 -    def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    1.34 -    def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
    1.35 +    def restrict(r: Range): Info[A] = Info(range.restrict(r), info)
    1.36 +    def try_restrict(r: Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
    1.37  
    1.38      def map[B](f: A => B): Info[B] = Info(range, f(info))
    1.39    }
    1.40 @@ -194,13 +194,13 @@
    1.41    trait Length
    1.42    {
    1.43      def apply(text: String): Int
    1.44 -    def offset(text: String, i: Int): Option[Text.Offset]
    1.45 +    def offset(text: String, i: Int): Option[Offset]
    1.46    }
    1.47  
    1.48    object Length extends Length
    1.49    {
    1.50      def apply(text: String): Int = text.length
    1.51 -    def offset(text: String, i: Int): Option[Text.Offset] =
    1.52 +    def offset(text: String, i: Int): Option[Offset] =
    1.53        if (0 <= i && i <= text.length) Some(i) else None
    1.54  
    1.55      val encodings: List[(String, Length)] =