# HG changeset patch
# User wenzelm
# Date 1282336501 -7200
# Node ID f7d7b805464841eb68d3a50030fb20905e29aecd
# Parent  3fa11fb01f868f018d7a6ad626131c02cda45518
Markup_Tree.select: misc simplification, proper restriction of parent in subtree;

diff -r 3fa11fb01f86 -r f7d7b8054648 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 22:32:15 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 22:35:01 2010 +0200
@@ -115,20 +115,20 @@
     new Markup_Tree(Branches.empty ++ bs)
   }
 
-  def select[A](range: Text.Range)(sel: PartialFunction[Any, A]): Stream[Node[List[A]]] =
+  def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] =
   {
-    def stream(parent: Node[List[A]], bs: Branches.T): Stream[Node[List[A]]] =
+    def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] =
     {
       val substream =
         (for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
           if (sel.isDefinedAt(node.info)) {
-            val current = Node(node.range.restrict(parent.range), List(sel(node.info)))
+            val current = Node(node.range.restrict(parent.range), sel(node.info))
             stream(current, subtree.branches)
           }
-          else stream(parent, subtree.branches)
+          else stream(parent.restrict(node.range), subtree.branches)
         }).flatten
 
-      def padding(last: Text.Offset, s: Stream[Node[List[A]]]): Stream[Node[List[A]]] =
+      def padding(last: Text.Offset, s: Stream[Node[A]]): Stream[Node[A]] =
         s match {
           case (node @ Node(Text.Range(start, stop), _)) #:: rest =>
             if (last < start)
@@ -142,7 +142,7 @@
       if (substream.isEmpty) Stream(parent)
       else padding(parent.range.start, substream)
     }
-    stream(Node(range, Nil), branches)
+    stream(root, branches)
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node[Any] => DefaultMutableTreeNode)