src/Pure/PIDE/markup_tree.scala
changeset 45459 a5c1599f664d
parent 45457 615ba724b269
child 45467 3f290b6288cf
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 16:25:32 2011 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 21:45:52 2011 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4  
     1.5  object Markup_Tree
     1.6  {
     1.7 +  type Cumulate[A] = PartialFunction[(A, Text.Markup), A]
     1.8    type Select[A] = PartialFunction[Text.Markup, A]
     1.9  
    1.10    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    1.11 @@ -83,6 +84,42 @@
    1.12      }
    1.13    }
    1.14  
    1.15 +  def cumulate[A](root: Text.Info[A])(result: Cumulate[A]): Stream[Text.Info[A]] =
    1.16 +  {
    1.17 +    def stream(
    1.18 +      last: Text.Offset,
    1.19 +      stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]): Stream[Text.Info[A]] =
    1.20 +    {
    1.21 +      stack match {
    1.22 +        case (parent, (range, (info, tree)) #:: more) :: rest =>
    1.23 +          val subrange = range.restrict(root.range)
    1.24 +          val subtree = tree.overlapping(subrange).toStream
    1.25 +          val start = subrange.start
    1.26 +
    1.27 +          val arg = (parent.info, info)
    1.28 +          if (result.isDefinedAt(arg)) {
    1.29 +            val next = Text.Info(subrange, result(arg))
    1.30 +            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    1.31 +            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    1.32 +            else nexts
    1.33 +          }
    1.34 +          else stream(last, (parent, subtree #::: more) :: rest)
    1.35 +
    1.36 +        case (parent, Stream.Empty) :: rest =>
    1.37 +          val stop = parent.range.stop
    1.38 +          val nexts = stream(stop, rest)
    1.39 +          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
    1.40 +          else nexts
    1.41 +
    1.42 +        case Nil =>
    1.43 +          val stop = root.range.stop
    1.44 +          if (last < stop) Stream(root.restrict(Text.Range(last, stop)))
    1.45 +          else Stream.empty
    1.46 +      }
    1.47 +    }
    1.48 +    stream(root.range.start, List((root, overlapping(root.range).toStream)))
    1.49 +  }
    1.50 +
    1.51    def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
    1.52    {
    1.53      def stream(