# HG changeset patch
# User wenzelm
# Date 1314264457 -7200
# Node ID 4f264fdf8d0ef5fbab8eb28bed42f9a8724352bb
# Parent  6f2943e34d60caedd9165b4c1167c27d2cdf5ddd
slightly more abstract Text.Perspective;

diff -r 6f2943e34d60 -r 4f264fdf8d0e src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Wed Aug 24 23:20:05 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Thu Aug 25 11:27:37 2011 +0200
@@ -62,28 +62,39 @@
 
   /* perspective */
 
-  type Perspective = List[Range]  // visible text partitioning in canonical order
-
-  def perspective(ranges: Seq[Range]): Perspective =
+  object Perspective
   {
-    val sorted_ranges = ranges.toArray
-    Sorting.quickSort(sorted_ranges)(Range.Ordering)
+    val empty = Perspective(Nil)
 
-    val result = new mutable.ListBuffer[Text.Range]
-    var last: Option[Text.Range] = None
-    for (range <- sorted_ranges)
+    def apply(ranges: Seq[Range]): Perspective =
     {
-      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)
+      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
+      new Perspective(result.toList)
     }
-    result ++= last
-    result.toList
+  }
+
+  sealed case class Perspective(ranges: List[Range]) // visible text partitioning in canonical order
+  {
+    def is_empty: Boolean = ranges.isEmpty
+    def range: Range =
+      if (is_empty) Range(0)
+      else Range(ranges.head.start, ranges.last.stop)
   }
 
 
diff -r 6f2943e34d60 -r 4f264fdf8d0e src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 23:20:05 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 25 11:27:37 2011 +0200
@@ -101,7 +101,7 @@
 
   def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
   {
-    if (perspective.isEmpty) Nil
+    if (perspective.is_empty) Nil
     else {
       val result = new mutable.ListBuffer[Command]
       @tailrec
@@ -120,8 +120,7 @@
           case _ =>
         }
       }
-      val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
-      check_ranges(perspective, node.command_range(perspective_range).toStream)
+      check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
       result.toList
     }
   }
diff -r 6f2943e34d60 -r 4f264fdf8d0e src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 23:20:05 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Aug 25 11:27:37 2011 +0200
@@ -74,10 +74,10 @@
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
-    Text.perspective(
+    Text.Perspective(
       for {
         doc_view <- Isabelle.document_views(buffer)
-        range <- doc_view.perspective()
+        range <- doc_view.perspective().ranges
       } yield range)
   }
 
@@ -88,7 +88,7 @@
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var pending_perspective = false
-    private var last_perspective: Text.Perspective = Nil
+    private var last_perspective: Text.Perspective = Text.Perspective.empty
 
     def snapshot(): List[Text.Edit] = pending.toList
 
diff -r 6f2943e34d60 -r 4f264fdf8d0e src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 24 23:20:05 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Aug 25 11:27:37 2011 +0200
@@ -118,7 +118,7 @@
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
-    Text.perspective(
+    Text.Perspective(
       for {
         i <- 0 until text_area.getVisibleLines
         val start = text_area.getScreenLineStartOffset(i)