src/Pure/PIDE/markup_tree.scala
changeset 38659 afac51977705
parent 38657 2e0ebdaac59b
child 38661 f1ba2ae8e58a
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Aug 24 20:36:48 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Aug 24 21:20:08 2010 +0200
     1.3 @@ -11,8 +11,6 @@
     1.4  import javax.swing.tree.DefaultMutableTreeNode
     1.5  
     1.6  import scala.collection.immutable.SortedMap
     1.7 -import scala.collection.mutable
     1.8 -import scala.annotation.tailrec
     1.9  
    1.10  
    1.11  object Markup_Tree
    1.12 @@ -32,14 +30,14 @@
    1.13      def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
    1.14      def single(entry: Entry): T = update(empty, entry)
    1.15  
    1.16 -    def overlapping(range: Text.Range, branches: T): T =
    1.17 +    def overlapping(range: Text.Range, branches: T): T =  // FIXME special cases!?
    1.18      {
    1.19        val start = Text.Range(range.start)
    1.20        val stop = Text.Range(range.stop)
    1.21 +      val bs = branches.range(start, stop)
    1.22        branches.get(stop) match {
    1.23 -        case Some(end) if range overlaps end._1.range =>
    1.24 -          update(branches.range(start, stop), end)
    1.25 -        case _ => branches.range(start, stop)
    1.26 +        case Some(end) if range overlaps end._1.range => update(bs, end)
    1.27 +        case _ => bs
    1.28        }
    1.29      }
    1.30    }
    1.31 @@ -66,7 +64,7 @@
    1.32          new Markup_Tree(Branches.update(branches, new_info -> empty))
    1.33        case Some((info, subtree)) =>
    1.34          val range = info.range
    1.35 -        if (range == new_range)
    1.36 +        if (range == new_range)  // FIXME append, not cons (!??)
    1.37            new Markup_Tree(Branches.update(branches,
    1.38              new_info -> new Markup_Tree(Branches.single((info, subtree)))))
    1.39          else if (range.contains(new_range))
    1.40 @@ -76,7 +74,7 @@
    1.41          else {
    1.42            val body = Branches.overlapping(new_range, branches)
    1.43            if (body.forall(e => new_range.contains(e._1))) {
    1.44 -            val rest = // branches -- body, with workarounds for Redblack in Scala 2.8.0
    1.45 +            val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0
    1.46                if (body.size > 1)
    1.47                  (Branches.empty /: branches)((rest, entry) =>
    1.48                    if (body.isDefinedAt(entry._1)) rest else rest + entry)
    1.49 @@ -91,37 +89,39 @@
    1.50      }
    1.51    }
    1.52  
    1.53 +  private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
    1.54 +    Branches.overlapping(range, branches).toStream
    1.55 +
    1.56    def select[A](root_range: Text.Range)
    1.57      (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
    1.58    {
    1.59 -    def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
    1.60 +    def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
    1.61 +      : Stream[Text.Info[A]] =
    1.62      {
    1.63 -      val range = parent.range
    1.64 -      val substream =
    1.65 -        (for ((info_range, (info, subtree)) <- Branches.overlapping(range, bs).toStream) yield {
    1.66 -          if (result.isDefinedAt(info)) {
    1.67 -            val current = Text.Info(info_range.restrict(range), result(info))
    1.68 -            stream(current, subtree.branches)
    1.69 -          }
    1.70 -          else stream(parent.restrict(info_range), subtree.branches)
    1.71 -        }).flatten
    1.72 +      stack match {
    1.73 +        case (parent, (range, (info, tree)) #:: more) :: rest =>
    1.74 +          val subrange = range.restrict(root_range)
    1.75 +          val subtree = tree.overlapping(subrange)
    1.76 +          val start = subrange.start
    1.77  
    1.78 -      def padding(last: Text.Offset, s: Stream[Text.Info[A]]): Stream[Text.Info[A]] =
    1.79 -        s match {
    1.80 -          case info #:: rest =>
    1.81 -            val Text.Range(start, stop) = info.range
    1.82 -            if (last < start)
    1.83 -              parent.restrict(Text.Range(last, start)) #:: info #:: padding(stop, rest)
    1.84 -            else info #:: padding(stop, rest)
    1.85 -          case Stream.Empty =>
    1.86 -            if (last < range.stop)
    1.87 -              Stream(parent.restrict(Text.Range(last, range.stop)))
    1.88 -            else Stream.Empty
    1.89 -        }
    1.90 -      if (substream.isEmpty) Stream(parent)
    1.91 -      else padding(range.start, substream)
    1.92 +          if (result.isDefinedAt(info)) {
    1.93 +            val next = Text.Info(subrange, result(info))
    1.94 +            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    1.95 +            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    1.96 +            else nexts
    1.97 +          }
    1.98 +          else stream(last, (parent, subtree #::: more) :: rest)
    1.99 +
   1.100 +        case (parent, Stream.Empty) :: rest =>
   1.101 +          val stop = parent.range.stop
   1.102 +          val nexts = stream(stop, rest)
   1.103 +          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
   1.104 +          else nexts
   1.105 +
   1.106 +        case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default))
   1.107 +      }
   1.108      }
   1.109 -    stream(Text.Info(root_range, default), branches)
   1.110 +    stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
   1.111    }
   1.112  
   1.113    def swing_tree(parent: DefaultMutableTreeNode)