# HG changeset patch
# User wenzelm
# Date 1347976529 -7200
# Node ID c5a8592fb5d3bd28cbf19f46cffabbfd30c519c3
# Parent  1053a564dd251e9bbee4d7d66de1108b2ec7a9ef
recover order of stacked markup;

diff -r 1053a564dd25 -r c5a8592fb5d3 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 18 14:51:12 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 18 15:55:29 2012 +0200
@@ -35,23 +35,30 @@
       else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
 
     def markup: List[XML.Elem] = rev_markup.reverse
+
+    def reverse_markup: Entry =
+      copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup)
   }
 
   object Branches
   {
     type T = SortedMap[Text.Range, Entry]
     val empty: T = SortedMap.empty(Text.Range.Ordering)
+
+    def reverse_markup(branches: T): T =
+      (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
   }
 }
 
 
 final class Markup_Tree private(branches: Markup_Tree.Branches.T)
 {
+  import Markup_Tree._
+
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))
 
-
-  import Markup_Tree._
+  def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches))
 
   override def toString =
     branches.toList.map(_._2) match {
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)