1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 17:01:58 2011 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 17:52:28 2011 +0100
     1.3 @@ -20,10 +20,10 @@
     1.4  
     1.5    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
     1.6  
     1.7 -  sealed case class Entry(range: Text.Range, rev_markup: List[XML.Tree], subtree: Markup_Tree)
     1.8 +  sealed case class Entry(range: Text.Range, rev_markup: List[XML.Elem], subtree: Markup_Tree)
     1.9    {
    1.10 -    def + (m: XML.Tree): Entry = copy(rev_markup = m :: rev_markup)
    1.11 -    def markup: List[XML.Tree] = rev_markup.reverse
    1.12 +    def + (m: XML.Elem): Entry = copy(rev_markup = m :: rev_markup)
    1.13 +    def markup: List[XML.Elem] = rev_markup.reverse
    1.14    }
    1.15  
    1.16    object Branches