src/Pure/General/xml.ML
changeset 38266 492d377ecfe2
parent 38228 ada3ab6b9085
child 38474 e498dc2eb576
     1.1 --- a/src/Pure/General/xml.ML	Tue Aug 10 20:13:52 2010 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Tue Aug 10 22:26:23 2010 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    datatype tree =
     1.5        Elem of Markup.T * tree list
     1.6      | Text of string
     1.7 +  type body = tree list
     1.8    val add_content: tree -> Buffer.T -> Buffer.T
     1.9    val header: string
    1.10    val text: string -> string
    1.11 @@ -35,6 +36,8 @@
    1.12      Elem of Markup.T * tree list
    1.13    | Text of string;
    1.14  
    1.15 +type body = tree list;
    1.16 +
    1.17  fun add_content (Elem (_, ts)) = fold add_content ts
    1.18    | add_content (Text s) = Buffer.add s;
    1.19