# HG changeset patch
# User wenzelm
# Date 1321116748 -3600
# Node ID 81b85d4ed2694d265056643a66830e556f43cf2b
# Parent  25306d92f4add211d447df51b9f9b18b1fb4bb17
more precise type;

diff -r 25306d92f4ad -r 81b85d4ed269 src/Pure/PIDE/markup_tree.scala
--- 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
diff -r 25306d92f4ad -r 81b85d4ed269 src/Pure/PIDE/text.scala
--- 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 */