src/Pure/PIDE/markup_tree.scala
changeset 55622 ce575c2212fc
parent 55620 19dffae33cde
child 55645 561754277494
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:08:39 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:56:51 2014 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4        var y = x
     1.5        var changed = false
     1.6        for {
     1.7 -        elem <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
     1.8 +        elem <- entry.markup
     1.9          if elements(elem.name)
    1.10          y1 <- result(y, Text.Info(entry.range, elem))
    1.11        } { y = y1; changed = true }