src/Pure/PIDE/document.scala

     def command_state(command: Command): Command.State
     def convert(i: Text.Offset): Text.Offset
     def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
+    def cumulate_markup[A](info: Text.Info[A])(result: Markup_Tree.Cumulate[A])
+      : Stream[Text.Info[A]]
     def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
       : Stream[Text.Info[Option[A]]]
   }
 
   type Assign =

         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
         def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
         def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
 
+        def cumulate_markup[A](root: Text.Info[A])(result: Markup_Tree.Cumulate[A])
+          : Stream[Text.Info[A]] =
+        {
+          val former_range = revert(root.range)
+          for {
+            (command, command_start) <- node.command_range(former_range).toStream
+            Text.Info(r0, a) <- command_state(command).markup.
+              cumulate(Text.Info((former_range - command_start).restrict(command.range), root.info)) {
+                case (a, Text.Info(r0, b))
+                if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
+                  result((a, Text.Info(convert(r0 + command_start), b)))
+              }
+          } yield Text.Info(convert(r0 + command_start), a)
+        }
+
         def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
           : Stream[Text.Info[Option[A]]] =
         {
           val former_range = revert(range)
           for {