proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
authorwenzelm
Fri Oct 21 22:44:55 2011 +0200 (2011-10-21 ago)
changeset 452409d97bd3c086a
parent 45239 ccea94064585
child 45241 87950f752099
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
clarified Text.Range apartness, with try_restrict and try_join operations;
private Perspective constructor to ensure abstract datatype integrity;
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/PIDE/text.scala	Fri Oct 21 17:39:07 2011 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Fri Oct 21 22:44:55 2011 +0200
     1.3 @@ -51,12 +51,19 @@
     1.4      def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
     1.5      def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
     1.6  
     1.7 +    def apart(that: Range): Boolean =
     1.8 +      (this.start max that.start) > (this.stop min that.stop)
     1.9 +
    1.10      def restrict(that: Range): Range =
    1.11        Range(this.start max that.start, this.stop min that.stop)
    1.12  
    1.13      def try_restrict(that: Range): Option[Range] =
    1.14 -      try { Some (restrict(that)) }
    1.15 -      catch { case ERROR(_) => None }
    1.16 +      if (this apart that) None
    1.17 +      else Some(restrict(that))
    1.18 +
    1.19 +    def try_join(that: Range): Option[Range] =
    1.20 +      if (this apart that) None
    1.21 +      else Some(Range(this.start min that.start, this.stop max that.stop))
    1.22    }
    1.23  
    1.24  
    1.25 @@ -68,33 +75,33 @@
    1.26  
    1.27      def apply(ranges: Seq[Range]): Perspective =
    1.28      {
    1.29 -      val sorted_ranges = ranges.toArray
    1.30 -      Sorting.quickSort(sorted_ranges)(Range.Ordering)
    1.31 -
    1.32        val result = new mutable.ListBuffer[Text.Range]
    1.33        var last: Option[Text.Range] = None
    1.34 -      for (range <- sorted_ranges)
    1.35 +      def ship(next: Option[Range]) { result ++= last; last = next }
    1.36 +
    1.37 +      for (range <- ranges.sortBy(_.start))
    1.38        {
    1.39          last match {
    1.40 -          case Some(last_range)
    1.41 -          if ((last_range overlaps range) || last_range.stop == range.start) =>
    1.42 -            last = Some(Text.Range(last_range.start, range.stop))
    1.43 -          case _ =>
    1.44 -            result ++= last
    1.45 -            last = Some(range)
    1.46 +          case None => ship(Some(range))
    1.47 +          case Some(last_range) =>
    1.48 +            last_range.try_join(range) match {
    1.49 +              case None => ship(Some(range))
    1.50 +              case joined => last = joined
    1.51 +            }
    1.52          }
    1.53        }
    1.54 -      result ++= last
    1.55 +      ship(None)
    1.56        new Perspective(result.toList)
    1.57      }
    1.58    }
    1.59  
    1.60 -  sealed case class Perspective(ranges: List[Range]) // visible text partitioning in canonical order
    1.61 +  class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order
    1.62    {
    1.63      def is_empty: Boolean = ranges.isEmpty
    1.64      def range: Range =
    1.65        if (is_empty) Range(0)
    1.66        else Range(ranges.head.start, ranges.last.stop)
    1.67 +    override def toString = ranges.toString
    1.68    }
    1.69  
    1.70