more precise type;

--- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 17:01:58 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 17:52:28 2011 +0100
@@ -20,10 +20,10 @@
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
-  sealed case class Entry(range: Text.Range, rev_markup: List[XML.Tree], subtree: Markup_Tree)
+  sealed case class Entry(range: Text.Range, rev_markup: List[XML.Elem], subtree: Markup_Tree)
   {
-    def + (m: XML.Tree): Entry = copy(rev_markup = m :: rev_markup)
-    def markup: List[XML.Tree] = rev_markup.reverse
+    def + (m: XML.Elem): Entry = copy(rev_markup = m :: rev_markup)
+    def markup: List[XML.Elem] = rev_markup.reverse
   }
 
   object Branches

--- a/src/Pure/PIDE/text.scala	Sat Nov 12 17:01:58 2011 +0100
+++ b/src/Pure/PIDE/text.scala	Sat Nov 12 17:52:28 2011 +0100
@@ -115,7 +115,7 @@
       catch { case ERROR(_) => None }
   }
 
-  type Markup = Info[XML.Tree]
+  type Markup = Info[XML.Elem]
 
 
   /* editing */