--- 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 {
--- 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)