src/Pure/General/xml.ML
changeset 14714 38ff9c8a7de0
parent 14713 6d203f6f0e8d
child 14728 df34201f1a15
equal deleted inserted replaced
14713:6d203f6f0e8d 14714:38ff9c8a7de0
    55 
    55 
    56 datatype tree =
    56 datatype tree =
    57     Elem of string * (string * string) list * tree list
    57     Elem of string * (string * string) list * tree list
    58   | Text of string;
    58   | Text of string;
    59 
    59 
    60 fun attribute (a, x) = a ^ " = " ^ "\"" (text x) "\"";
    60 fun attribute (a, x) = a ^ " = \"" ^ (text x) ^ "\"";
    61 
    61 
    62 fun element name atts cs =
    62 fun element name atts cs =
    63   let val elem = space_implode " " (name :: map attribute atts) in
    63   let val elem = space_implode " " (name :: map attribute atts) in
    64     if null cs then enclose "<" "/>" elem
    64     if null cs then enclose "<" "/>" elem
    65     else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
    65     else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name