# HG changeset patch
# User wenzelm
# Date 1314022343 -7200
# Node ID 1079ab6b342b1ec58c6ee2b700004576c669a919
# Parent  81b4af4cfa5aca295e0bb49db806e3cd07a7722d
added official Text.Range.Ordering;
some support for text perspective;

diff -r 81b4af4cfa5a -r 1079ab6b342b src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Mon Aug 22 14:15:52 2011 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Mon Aug 22 16:12:23 2011 +0200
@@ -22,10 +22,7 @@
     type Entry = (Text.Info[Any], Markup_Tree)
     type T = SortedMap[Text.Range, Entry]
 
-    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
-      {
-        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
-      })
+    val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
 
     def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
     def single(entry: Entry): T = update(empty, entry)
diff -r 81b4af4cfa5a -r 1079ab6b342b 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)
diff -r 81b4af4cfa5a -r 1079ab6b342b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 14:15:52 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 16:12:23 2011 +0200
@@ -99,6 +99,19 @@
   }
 
 
+  /* perspective */
+
+  def perspective(): Text.Perspective =
+  {
+    Swing_Thread.require()
+    Text.perspective(
+      for {
+        doc_view <- Isabelle.document_views(buffer)
+        range <- doc_view.perspective()
+      } yield range)
+  }
+
+
   /* snapshot */
 
   def snapshot(): Document.Snapshot =
diff -r 81b4af4cfa5a -r 1079ab6b342b src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 14:15:52 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 16:12:23 2011 +0200
@@ -10,6 +10,7 @@
 
 import isabelle._
 
+import scala.collection.mutable
 import scala.actors.Actor._
 
 import java.lang.System
@@ -111,6 +112,22 @@
   }
 
 
+  /* perspective */
+
+  def perspective(): Text.Perspective =
+  {
+    Swing_Thread.require()
+    Text.perspective(
+      for {
+        i <- 0 until text_area.getVisibleLines
+        val start = text_area.getScreenLineStartOffset(i)
+        val stop = text_area.getScreenLineEndOffset(i)
+        if start >= 0 && stop >= 0
+      }
+      yield Text.Range(start, stop))
+  }
+
+
   /* snapshot */
 
   // owned by Swing thread
diff -r 81b4af4cfa5a -r 1079ab6b342b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 14:15:52 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 16:12:23 2011 +0200
@@ -199,6 +199,13 @@
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
 
+  def document_views(buffer: Buffer): List[Document_View] =
+    for {
+      text_area <- jedit_text_areas(buffer).toList
+      val doc_view = document_view(text_area)
+      if doc_view.isDefined
+    } yield doc_view.get
+
   def init_model(buffer: Buffer)
   {
     swing_buffer_lock(buffer) {