src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Mon Aug 22 14:15:52 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Aug 22 16:12:23 2011 +0200
@@ -8,6 +8,11 @@
 package isabelle
 
 
+import scala.collection.mutable
+import scala.math.Ordering
+import scala.util.Sorting
+
+
 object Text
 {
   /* offset */
@@ -20,6 +25,11 @@
   object Range
   {
     def apply(start: Offset): Range = Range(start, start)
+
+    object Ordering extends scala.math.Ordering[Text.Range]
+    {
+      def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
+    }
   }
 
   sealed case class Range(val start: Offset, val stop: Offset)
@@ -50,6 +60,33 @@
   }
 
 
+  /* perspective */
+
+  type Perspective = List[Range]  // partitioning in canonical order
+
+  def perspective(ranges: Seq[Range]): Perspective =
+  {
+    val sorted_ranges = ranges.toArray
+    Sorting.quickSort(sorted_ranges)(Range.Ordering)
+
+    val result = new mutable.ListBuffer[Text.Range]
+    var last: Option[Text.Range] = None
+    for (range <- sorted_ranges)
+    {
+      last match {
+        case Some(last_range)
+        if ((last_range overlaps range) || last_range.stop == range.start) =>
+          last = Some(Text.Range(last_range.start, range.stop))
+        case _ =>
+          result ++= last
+          last = Some(range)
+      }
+    }
+    result ++= last
+    result.toList
+  }
+
+
   /* information associated with text range */
 
   sealed case class Info[A](val range: Text.Range, val info: A)