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