src/Pure/General/yxml.ML
changeset 38228 ada3ab6b9085
parent 34095 c2f176a38448
child 38265 cc9fde54311f
     1.1 --- a/src/Pure/General/yxml.ML	Sat Aug 07 19:52:14 2010 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Sat Aug 07 21:03:06 2010 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4      fun attrib (a, x) =
     1.5        Buffer.add Y #>
     1.6        Buffer.add a #> Buffer.add "=" #> Buffer.add x;
     1.7 -    fun tree (XML.Elem (name, atts, ts)) =
     1.8 +    fun tree (XML.Elem ((name, atts), ts)) =
     1.9            Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
    1.10            fold tree ts #>
    1.11            Buffer.add XYX
    1.12 @@ -104,7 +104,7 @@
    1.13    | push name atts pending = ((name, atts), []) :: pending;
    1.14  
    1.15  fun pop ((("", _), _) :: _) = err_unbalanced ""
    1.16 -  | pop (((name, atts), body) :: pending) = add (XML.Elem (name, atts, rev body)) pending;
    1.17 +  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
    1.18  
    1.19  
    1.20  (* parsing *)