diff -r 1053a564dd25 -r c5a8592fb5d3 src/Pure/PIDE/xml.scala --- 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)