src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 16:25:32 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 21:45:52 2011 +0100
@@ -15,6 +15,7 @@
 
 object Markup_Tree
 {
+  type Cumulate[A] = PartialFunction[(A, Text.Markup), A]
   type Select[A] = PartialFunction[Text.Markup, A]
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
@@ -83,6 +84,42 @@
     }
   }
 
+  def cumulate[A](root: Text.Info[A])(result: Cumulate[A]): Stream[Text.Info[A]] =
+  {
+    def stream(
+      last: Text.Offset,
+      stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]): Stream[Text.Info[A]] =
+    {
+      stack match {
+        case (parent, (range, (info, tree)) #:: more) :: rest =>
+          val subrange = range.restrict(root.range)
+          val subtree = tree.overlapping(subrange).toStream
+          val start = subrange.start
+
+          val arg = (parent.info, info)
+          if (result.isDefinedAt(arg)) {
+            val next = Text.Info(subrange, result(arg))
+            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
+            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
+            else nexts
+          }
+          else stream(last, (parent, subtree #::: more) :: rest)
+
+        case (parent, Stream.Empty) :: rest =>
+          val stop = parent.range.stop
+          val nexts = stream(stop, rest)
+          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
+          else nexts
+
+        case Nil =>
+          val stop = root.range.stop
+          if (last < stop) Stream(root.restrict(Text.Range(last, stop)))
+          else Stream.empty
+      }
+    }
+    stream(root.range.start, List((root, overlapping(root.range).toStream)))
+  }
+
   def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
   {
     def stream(