src/Pure/PIDE/markup_tree.scala
changeset 52889 ea3338812e67
parent 52642 84eb792224a8
child 52900 d29bf6db8a2d
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 11:50:14 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 13:46:32 2013 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4      to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
     1.5  
     1.6    def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
     1.7 -    result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
     1.8 +    result: (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
     1.9    {
    1.10      val notable: Elements => Boolean =
    1.11        result_elements match {
    1.12 @@ -233,15 +233,12 @@
    1.13  
    1.14      def results(x: A, entry: Entry): Option[A] =
    1.15      {
    1.16 -      val (y, changed) =
    1.17 -        // FIXME proper cumulation order (including status markup) (!?)
    1.18 -        ((x, false) /: entry.rev_markup)((res, info) =>
    1.19 -          {
    1.20 -            val (y, changed) = res
    1.21 -            val arg = (y, Text.Info(entry.range, info))
    1.22 -            if (result.isDefinedAt(arg)) (result(arg), true)
    1.23 -            else res
    1.24 -          })
    1.25 +      var y = x
    1.26 +      var changed = false
    1.27 +      for {
    1.28 +        info <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
    1.29 +        y1 <- result(y, Text.Info(entry.range, info))
    1.30 +      } { y = y1; changed = true }
    1.31        if (changed) Some(y) else None
    1.32      }
    1.33