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