--- a/src/Pure/PIDE/markup_tree.scala Tue Sep 07 21:06:58 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Tue Sep 07 22:28:58 2010 +0200
@@ -89,11 +89,13 @@
private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
Branches.overlapping(range, branches).toStream
- def select[A](root_range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+ def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+ : Stream[Text.Info[Option[A]]] =
{
- def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
- : Stream[Text.Info[A]] =
+ def stream(
+ last: Text.Offset,
+ stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
+ : Stream[Text.Info[Option[A]]] =
{
stack match {
case (parent, (range, (info, tree)) #:: more) :: rest =>
@@ -102,7 +104,7 @@
val start = subrange.start
if (result.isDefinedAt(info)) {
- val next = Text.Info(subrange, result(info))
+ val next = Text.Info[Option[A]](subrange, Some(result(info)))
val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
else nexts
@@ -117,12 +119,11 @@
case Nil =>
val stop = root_range.stop
- if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
+ if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
else Stream.empty
}
}
- stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
- .iterator
+ stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
}
def swing_tree(parent: DefaultMutableTreeNode)