diff -r b8fdd3ae8815 -r 0468964aec11 src/Pure/PIDE/markup_tree.scala
--- 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)