src/Pure/PIDE/text.scala
changeset 44379 1079ab6b342b
parent 43714 3749d1e6dde9
child 44384 8f6054a63f96
     1.1 --- a/src/Pure/PIDE/text.scala	Mon Aug 22 14:15:52 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Mon Aug 22 16:12:23 2011 +0200
     1.3 @@ -8,6 +8,11 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.collection.mutable
     1.8 +import scala.math.Ordering
     1.9 +import scala.util.Sorting
    1.10 +
    1.11 +
    1.12  object Text
    1.13  {
    1.14    /* offset */
    1.15 @@ -20,6 +25,11 @@
    1.16    object Range
    1.17    {
    1.18      def apply(start: Offset): Range = Range(start, start)
    1.19 +
    1.20 +    object Ordering extends scala.math.Ordering[Text.Range]
    1.21 +    {
    1.22 +      def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    1.23 +    }
    1.24    }
    1.25  
    1.26    sealed case class Range(val start: Offset, val stop: Offset)
    1.27 @@ -50,6 +60,33 @@
    1.28    }
    1.29  
    1.30  
    1.31 +  /* perspective */
    1.32 +
    1.33 +  type Perspective = List[Range]  // partitioning in canonical order
    1.34 +
    1.35 +  def perspective(ranges: Seq[Range]): Perspective =
    1.36 +  {
    1.37 +    val sorted_ranges = ranges.toArray
    1.38 +    Sorting.quickSort(sorted_ranges)(Range.Ordering)
    1.39 +
    1.40 +    val result = new mutable.ListBuffer[Text.Range]
    1.41 +    var last: Option[Text.Range] = None
    1.42 +    for (range <- sorted_ranges)
    1.43 +    {
    1.44 +      last match {
    1.45 +        case Some(last_range)
    1.46 +        if ((last_range overlaps range) || last_range.stop == range.start) =>
    1.47 +          last = Some(Text.Range(last_range.start, range.stop))
    1.48 +        case _ =>
    1.49 +          result ++= last
    1.50 +          last = Some(range)
    1.51 +      }
    1.52 +    }
    1.53 +    result ++= last
    1.54 +    result.toList
    1.55 +  }
    1.56 +
    1.57 +
    1.58    /* information associated with text range */
    1.59  
    1.60    sealed case class Info[A](val range: Text.Range, val info: A)