1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 20:11:17 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 20:25:15 2010 +0200
     1.3 @@ -83,8 +83,8 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def select[A](root: Text.Info[A])
     1.8 -    (result: PartialFunction[Text.Info[Any], A]): Stream[Text.Info[A]] =
     1.9 +  def select[A](root_range: Text.Range)
    1.10 +    (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
    1.11    {
    1.12      def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
    1.13      {
    1.14 @@ -113,7 +113,7 @@
    1.15        if (substream.isEmpty) Stream(parent)
    1.16        else padding(range.start, substream)
    1.17      }
    1.18 -    stream(root, branches)
    1.19 +    stream(Text.Info(root_range, default), branches)
    1.20    }
    1.21  
    1.22    def swing_tree(parent: DefaultMutableTreeNode)