src/Pure/PIDE/markup_tree.scala
changeset 38845 a9e37daf5bd0
parent 38726 6d5f9af42eca
child 39177 0468964aec11
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Aug 28 22:58:24 2010 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 29 15:09:11 2010 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4      Branches.overlapping(range, branches).toStream
     1.5  
     1.6    def select[A](root_range: Text.Range)
     1.7 -    (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
     1.8 +    (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
     1.9    {
    1.10      def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
    1.11        : Stream[Text.Info[A]] =
    1.12 @@ -122,6 +122,7 @@
    1.13        }
    1.14      }
    1.15      stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
    1.16 +      .iterator
    1.17    }
    1.18  
    1.19    def swing_tree(parent: DefaultMutableTreeNode)