--- a/src/Pure/PIDE/document.scala Fri Nov 11 16:25:32 2011 +0100
+++ b/src/Pure/PIDE/document.scala Fri Nov 11 21:45:52 2011 +0100
@@ -240,6 +240,8 @@
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]]]
}
@@ -471,6 +473,21 @@
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]]] =
{
--- 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(