1.1 --- a/src/Pure/PIDE/text.scala	Wed Aug 24 23:20:05 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Thu Aug 25 11:27:37 2011 +0200
     1.3 @@ -62,28 +62,39 @@
     1.4  
     1.5    /* perspective */
     1.6  
     1.7 -  type Perspective = List[Range]  // visible text partitioning in canonical order
     1.8 -
     1.9 -  def perspective(ranges: Seq[Range]): Perspective =
    1.10 +  object Perspective
    1.11    {
    1.12 -    val sorted_ranges = ranges.toArray
    1.13 -    Sorting.quickSort(sorted_ranges)(Range.Ordering)
    1.14 +    val empty = Perspective(Nil)
    1.15  
    1.16 -    val result = new mutable.ListBuffer[Text.Range]
    1.17 -    var last: Option[Text.Range] = None
    1.18 -    for (range <- sorted_ranges)
    1.19 +    def apply(ranges: Seq[Range]): Perspective =
    1.20      {
    1.21 -      last match {
    1.22 -        case Some(last_range)
    1.23 -        if ((last_range overlaps range) || last_range.stop == range.start) =>
    1.24 -          last = Some(Text.Range(last_range.start, range.stop))
    1.25 -        case _ =>
    1.26 -          result ++= last
    1.27 -          last = Some(range)
    1.28 +      val sorted_ranges = ranges.toArray
    1.29 +      Sorting.quickSort(sorted_ranges)(Range.Ordering)
    1.30 +
    1.31 +      val result = new mutable.ListBuffer[Text.Range]
    1.32 +      var last: Option[Text.Range] = None
    1.33 +      for (range <- sorted_ranges)
    1.34 +      {
    1.35 +        last match {
    1.36 +          case Some(last_range)
    1.37 +          if ((last_range overlaps range) || last_range.stop == range.start) =>
    1.38 +            last = Some(Text.Range(last_range.start, range.stop))
    1.39 +          case _ =>
    1.40 +            result ++= last
    1.41 +            last = Some(range)
    1.42 +        }
    1.43        }
    1.44 +      result ++= last
    1.45 +      new Perspective(result.toList)
    1.46      }
    1.47 -    result ++= last
    1.48 -    result.toList
    1.49 +  }
    1.50 +
    1.51 +  sealed case class Perspective(ranges: List[Range]) // visible text partitioning in canonical order
    1.52 +  {
    1.53 +    def is_empty: Boolean = ranges.isEmpty
    1.54 +    def range: Range =
    1.55 +      if (is_empty) Range(0)
    1.56 +      else Range(ranges.head.start, ranges.last.stop)
    1.57    }
    1.58  
    1.59