equal
deleted
inserted
replaced
39 | decode "&" = "&" |
39 | decode "&" = "&" |
40 | decode "'" = "'" |
40 | decode "'" = "'" |
41 | decode """ = "\"" |
41 | decode """ = "\"" |
42 | decode c = c; |
42 | decode c = c; |
43 |
43 |
44 val text = implode o map encode o explode; |
44 val text = String.translate (encode o String.str); |
45 |
45 |
46 |
46 |
47 (* elements *) |
47 (* elements *) |
48 |
48 |
49 datatype tree = |
49 datatype tree = |
50 Elem of string * (string * string) list * tree list |
50 Elem of string * (string * string) list * tree list |
51 | Text of string; |
51 | Text of string; |
52 |
52 |
53 fun attribute (a, x) = a ^ " = " ^ quote (text x); |
53 fun attribute (a, x) = a ^ " = " ^ Library.quote (text x); |
54 |
54 |
55 fun element name atts cs = |
55 fun element name atts cs = |
56 let val elem = space_implode " " (name :: map attribute atts) in |
56 let val elem = space_implode " " (name :: map attribute atts) in |
57 if null cs then enclose "<" "/>" elem |
57 if null cs then enclose "<" "/>" elem |
58 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
58 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |