more precise type;
authorwenzelm
Sat Nov 12 17:52:28 2011 +0100 (2011-11-12)
changeset 4547081b85d4ed269
parent 45469 25306d92f4ad
child 45471 489f27dcc0f4
more precise type;
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
     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
     2.1 --- a/src/Pure/PIDE/text.scala	Sat Nov 12 17:01:58 2011 +0100
     2.2 +++ b/src/Pure/PIDE/text.scala	Sat Nov 12 17:52:28 2011 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4        catch { case ERROR(_) => None }
     2.5    }
     2.6  
     2.7 -  type Markup = Info[XML.Tree]
     2.8 +  type Markup = Info[XML.Elem]
     2.9  
    2.10  
    2.11    /* editing */