equal
deleted
inserted
replaced
|
1 (* Title: Pure/General/xml.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, LMU München |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Basic support for XML output. |
|
7 *) |
|
8 |
|
9 signature XML = |
|
10 sig |
|
11 val element: string -> (string * string) list -> string list -> string |
|
12 val text: string -> string |
|
13 val header: string |
|
14 end; |
|
15 |
|
16 structure XML: XML = |
|
17 struct |
|
18 |
|
19 (* character data *) |
|
20 |
|
21 fun encode "<" = "<" |
|
22 | encode ">" = ">" |
|
23 | encode "&" = "&" |
|
24 | encode "'" = "'" |
|
25 | encode "\"" = """ |
|
26 | encode c = c; |
|
27 |
|
28 val text = implode o map encode o explode; |
|
29 |
|
30 |
|
31 (* elements *) |
|
32 |
|
33 fun attribute (a, x) = a ^ " = " ^ quote (text x); |
|
34 |
|
35 fun element name atts cs = |
|
36 let val elem = space_implode " " (name :: map attribute atts) in |
|
37 if null cs then enclose "<" "/>" elem |
|
38 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
|
39 end; |
|
40 |
|
41 val header = "<?xml version=\"1.0\"?>\n"; |
|
42 |
|
43 end; |