--- a/src/Pure/PIDE/markup_tree.scala Sat Aug 28 22:58:24 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Sun Aug 29 15:09:11 2010 +0200
@@ -90,7 +90,7 @@
Branches.overlapping(range, branches).toStream
def select[A](root_range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
+ (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
{
def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
: Stream[Text.Info[A]] =
@@ -122,6 +122,7 @@
}
}
stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
+ .iterator
}
def swing_tree(parent: DefaultMutableTreeNode)