misc tuning and simplification;
authorwenzelm
Sun Aug 22 19:33:01 2010 +0200 (2010-08-22)
changeset 385781ebc6b76e5ff
parent 38577 4e4d3ea3725a
child 38579 ce46a6f55bce
misc tuning and simplification;
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 18:46:16 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 19:33:01 2010 +0200
     1.3 @@ -22,19 +22,19 @@
     1.4    object Branches
     1.5    {
     1.6      type Entry = (Text.Info[Any], Markup_Tree)
     1.7 -    type T = SortedMap[Text.Info[Any], Entry]
     1.8 +    type T = SortedMap[Text.Range, Entry]
     1.9  
    1.10 -    val empty = SortedMap.empty[Text.Info[Any], Entry](new scala.math.Ordering[Text.Info[Any]]
    1.11 +    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
    1.12        {
    1.13 -        def compare(x: Text.Info[Any], y: Text.Info[Any]): Int = x.range compare y.range
    1.14 +        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    1.15        })
    1.16  
    1.17 -    def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
    1.18 +    def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
    1.19  
    1.20      def overlapping(range: Text.Range, branches: T): T =
    1.21      {
    1.22 -      val start = Text.Info[Any](Text.Range(range.start), Nil)
    1.23 -      val stop = Text.Info[Any](Text.Range(range.stop), Nil)
    1.24 +      val start = Text.Range(range.start)
    1.25 +      val stop = Text.Range(range.stop)
    1.26        branches.get(stop) match {
    1.27          case Some(end) if range overlaps end._1.range =>
    1.28            update(branches.range(start, stop), end)
    1.29 @@ -59,17 +59,19 @@
    1.30  
    1.31    def + (new_info: Text.Info[Any]): Markup_Tree =
    1.32    {
    1.33 -    branches.get(new_info) match {
    1.34 +    val new_range = new_info.range
    1.35 +    branches.get(new_range) match {
    1.36        case None =>
    1.37          new Markup_Tree(Branches.update(branches, new_info -> empty))
    1.38        case Some((info, subtree)) =>
    1.39 -        if (info.range != new_info.range && info.contains(new_info))
    1.40 +        val range = info.range
    1.41 +        if (range != new_range && range.contains(new_range))
    1.42            new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
    1.43 -        else if (new_info.contains(branches.head._1) && new_info.contains(branches.last._1))
    1.44 +        else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
    1.45            new Markup_Tree(Branches.update(Branches.empty, (new_info -> this)))
    1.46          else {
    1.47 -          val body = Branches.overlapping(new_info.range, branches)
    1.48 -          if (body.forall(e => new_info.contains(e._1))) {
    1.49 +          val body = Branches.overlapping(new_range, branches)
    1.50 +          if (body.forall(e => new_range.contains(e._1))) {
    1.51              val rest = (branches /: body) { case (bs, (e, _)) => bs - e }
    1.52              new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
    1.53            }
    1.54 @@ -81,17 +83,19 @@
    1.55      }
    1.56    }
    1.57  
    1.58 -  def select[A](root: Text.Info[A])(sel: PartialFunction[Text.Info[Any], A]): Stream[Text.Info[A]] =
    1.59 +  def select[A](root: Text.Info[A])
    1.60 +    (result: PartialFunction[Text.Info[Any], A]): Stream[Text.Info[A]] =
    1.61    {
    1.62      def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
    1.63      {
    1.64 +      val range = parent.range
    1.65        val substream =
    1.66 -        (for ((_, (info, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
    1.67 -          if (sel.isDefinedAt(info)) {
    1.68 -            val current = Text.Info(info.range.restrict(parent.range), sel(info))
    1.69 +        (for ((info_range, (info, subtree)) <- Branches.overlapping(range, bs).toStream) yield {
    1.70 +          if (result.isDefinedAt(info)) {
    1.71 +            val current = Text.Info(info_range.restrict(range), result(info))
    1.72              stream(current, subtree.branches)
    1.73            }
    1.74 -          else stream(parent.restrict(info.range), subtree.branches)
    1.75 +          else stream(parent.restrict(info_range), subtree.branches)
    1.76          }).flatten
    1.77  
    1.78        def padding(last: Text.Offset, s: Stream[Text.Info[A]]): Stream[Text.Info[A]] =
    1.79 @@ -102,12 +106,12 @@
    1.80                parent.restrict(Text.Range(last, start)) #:: info #:: padding(stop, rest)
    1.81              else info #:: padding(stop, rest)
    1.82            case Stream.Empty =>
    1.83 -            if (last < parent.range.stop)
    1.84 -              Stream(parent.restrict(Text.Range(last, parent.range.stop)))
    1.85 +            if (last < range.stop)
    1.86 +              Stream(parent.restrict(Text.Range(last, range.stop)))
    1.87              else Stream.Empty
    1.88          }
    1.89        if (substream.isEmpty) Stream(parent)
    1.90 -      else padding(parent.range.start, substream)
    1.91 +      else padding(range.start, substream)
    1.92      }
    1.93      stream(root, branches)
    1.94    }
     2.1 --- a/src/Pure/PIDE/text.scala	Sun Aug 22 18:46:16 2010 +0200
     2.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 22 19:33:01 2010 +0200
     2.3 @@ -46,7 +46,6 @@
     2.4  
     2.5    case class Info[A](val range: Text.Range, val info: A)
     2.6    {
     2.7 -    def contains[B](that: Info[B]): Boolean = this.range contains that.range
     2.8      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
     2.9    }
    2.10