equal
deleted
inserted
replaced
46 | encode "\"" = """ |
46 | encode "\"" = """ |
47 | encode c = c; |
47 | encode c = c; |
48 |
48 |
49 val text = Library.translate_string encode; |
49 val text = Library.translate_string encode; |
50 |
50 |
51 val cdata = enclose "<![CDATA[" "]]>"; |
51 val cdata = enclose "<![CDATA[" "]]>\n" |
52 |
52 |
53 |
53 |
54 (* elements *) |
54 (* elements *) |
55 |
55 |
56 fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\""; |
56 fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\""; |
58 fun element name atts cs = |
58 fun element name atts cs = |
59 let val elem = space_implode " " (name :: map attribute atts) in |
59 let val elem = space_implode " " (name :: map attribute atts) in |
60 if null cs then enclose "<" "/>" elem |
60 if null cs then enclose "<" "/>" elem |
61 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
61 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
62 end; |
62 end; |
|
63 |
63 |
64 |
64 |
65 |
65 |
66 |
66 (** explicit XML trees **) |
67 (** explicit XML trees **) |
67 |
68 |