src/Pure/PIDE/xml.scala
changeset 49417 c5a8592fb5d3
parent 49416 1053a564dd25
child 49465 76ecbc7f3683
--- a/src/Pure/PIDE/xml.scala	Tue Sep 18 14:51:12 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Tue Sep 18 15:55:29 2012 +0200
@@ -82,7 +82,6 @@
           val offset = text.length
           trees.foreach(traverse)
           val end_offset = text.length
-          // FIXME proper order!?
           if (record_markup)
             markup_tree +=
               isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
@@ -90,7 +89,7 @@
       }
 
     body.foreach(traverse)
-    (text.toString, markup_tree)
+    (text.toString, markup_tree.reverse_markup)
   }
 
   def content_markup(body: Body): (String, Markup_Tree) = make_content(body, true)