src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:08:39 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:56:51 2014 +0100
@@ -230,7 +230,7 @@
       var y = x
       var changed = false
       for {
-        elem <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
+        elem <- entry.markup
         if elements(elem.name)
         y1 <- result(y, Text.Info(entry.range, elem))
       } { y = y1; changed = true }