recover order of stacked markup;
authorwenzelm
Tue Sep 18 15:55:29 2012 +0200 (2012-09-18)
changeset 49417c5a8592fb5d3
parent 49416 1053a564dd25
child 49418 c451856129cd
recover order of stacked markup;
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/xml.scala
     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 {
     2.1 --- a/src/Pure/PIDE/xml.scala	Tue Sep 18 14:51:12 2012 +0200
     2.2 +++ b/src/Pure/PIDE/xml.scala	Tue Sep 18 15:55:29 2012 +0200
     2.3 @@ -82,7 +82,6 @@
     2.4            val offset = text.length
     2.5            trees.foreach(traverse)
     2.6            val end_offset = text.length
     2.7 -          // FIXME proper order!?
     2.8            if (record_markup)
     2.9              markup_tree +=
    2.10                isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
    2.11 @@ -90,7 +89,7 @@
    2.12        }
    2.13  
    2.14      body.foreach(traverse)
    2.15 -    (text.toString, markup_tree)
    2.16 +    (text.toString, markup_tree.reverse_markup)
    2.17    }
    2.18  
    2.19    def content_markup(body: Body): (String, Markup_Tree) = make_content(body, true)