src/Pure/PIDE/markup_tree.scala
changeset 39177 0468964aec11
parent 38845 a9e37daf5bd0
child 39178 83e9f3ccea9f
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 21:06:58 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 22:28:58 2010 +0200
     1.3 @@ -89,11 +89,13 @@
     1.4    private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
     1.5      Branches.overlapping(range, branches).toStream
     1.6  
     1.7 -  def select[A](root_range: Text.Range)
     1.8 -    (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
     1.9 +  def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
    1.10 +    : Stream[Text.Info[Option[A]]] =
    1.11    {
    1.12 -    def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
    1.13 -      : Stream[Text.Info[A]] =
    1.14 +    def stream(
    1.15 +      last: Text.Offset,
    1.16 +      stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
    1.17 +        : Stream[Text.Info[Option[A]]] =
    1.18      {
    1.19        stack match {
    1.20          case (parent, (range, (info, tree)) #:: more) :: rest =>
    1.21 @@ -102,7 +104,7 @@
    1.22            val start = subrange.start
    1.23  
    1.24            if (result.isDefinedAt(info)) {
    1.25 -            val next = Text.Info(subrange, result(info))
    1.26 +            val next = Text.Info[Option[A]](subrange, Some(result(info)))
    1.27              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    1.28              if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    1.29              else nexts
    1.30 @@ -117,12 +119,11 @@
    1.31  
    1.32          case Nil =>
    1.33            val stop = root_range.stop
    1.34 -          if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
    1.35 +          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
    1.36            else Stream.empty
    1.37        }
    1.38      }
    1.39 -    stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
    1.40 -      .iterator
    1.41 +    stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
    1.42    }
    1.43  
    1.44    def swing_tree(parent: DefaultMutableTreeNode)