src/Pure/PIDE/markup_tree.scala
changeset 49417 c5a8592fb5d3
parent 48762 9ff86bf6ad19
child 49465 76ecbc7f3683
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 18 14:51:12 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 18 15:55:29 2012 +0200
     1.3 @@ -35,23 +35,30 @@
     1.4        else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
     1.5  
     1.6      def markup: List[XML.Elem] = rev_markup.reverse
     1.7 +
     1.8 +    def reverse_markup: Entry =
     1.9 +      copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup)
    1.10    }
    1.11  
    1.12    object Branches
    1.13    {
    1.14      type T = SortedMap[Text.Range, Entry]
    1.15      val empty: T = SortedMap.empty(Text.Range.Ordering)
    1.16 +
    1.17 +    def reverse_markup(branches: T): T =
    1.18 +      (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
    1.19    }
    1.20  }
    1.21  
    1.22  
    1.23  final class Markup_Tree private(branches: Markup_Tree.Branches.T)
    1.24  {
    1.25 +  import Markup_Tree._
    1.26 +
    1.27    private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
    1.28      this(branches + (entry.range -> entry))
    1.29  
    1.30 -
    1.31 -  import Markup_Tree._
    1.32 +  def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches))
    1.33  
    1.34    override def toString =
    1.35      branches.toList.map(_._2) match {