1 (* Title: Pure/General/xml.ML |
1 (* Title: Pure/General/xml.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David Aspinall, Stefan Berghofer and Markus Wenzel |
3 Author: David Aspinall, Stefan Berghofer and Markus Wenzel |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 Basic support for XML input and output. |
6 Basic support for XML. |
7 *) |
7 *) |
8 |
8 |
9 signature XML = |
9 signature XML = |
10 sig |
10 sig |
|
11 val header: string |
|
12 val text: string -> string |
|
13 val cdata: string -> string |
|
14 val element: string -> (string * string) list -> string list -> string |
11 datatype tree = |
15 datatype tree = |
12 Elem of string * (string * string) list * tree list |
16 Elem of string * (string * string) list * tree list |
13 | Text of string |
17 | Text of string |
14 val element: string -> (string * string) list -> string list -> string |
|
15 val text: string -> string |
|
16 val cdata: string -> string |
|
17 val header: string |
|
18 val string_of_tree: tree -> string |
18 val string_of_tree: tree -> string |
19 val tree_of_string: string -> tree |
|
20 val parse_content: string list -> tree list * string list |
19 val parse_content: string list -> tree list * string list |
21 val parse_elem: string list -> tree * string list |
20 val parse_elem: string list -> tree * string list |
22 val parse_document: string list -> (string option * tree) * string list |
21 val parse_document: string list -> (string option * tree) * string list |
|
22 val tree_of_string: string -> tree |
23 end; |
23 end; |
24 |
24 |
25 structure XML: XML = |
25 structure XML: XML = |
26 struct |
26 struct |
27 |
27 |
28 (* character data *) |
28 (** string based representation (small scale) **) |
|
29 |
|
30 val header = "<?xml version=\"1.0\"?>\n"; |
|
31 |
|
32 |
|
33 (* text and character data *) |
|
34 |
|
35 fun decode "<" = "<" |
|
36 | decode ">" = ">" |
|
37 | decode "&" = "&" |
|
38 | decode "'" = "'" |
|
39 | decode """ = "\"" |
|
40 | decode c = c; |
29 |
41 |
30 fun encode "<" = "<" |
42 fun encode "<" = "<" |
31 | encode ">" = ">" |
43 | encode ">" = ">" |
32 | encode "&" = "&" |
44 | encode "&" = "&" |
33 | encode "'" = "'" |
45 | encode "'" = "'" |
34 | encode "\"" = """ |
46 | encode "\"" = """ |
35 | encode c = c; |
47 | encode c = c; |
36 |
48 |
37 fun decode "<" = "<" |
|
38 | decode ">" = ">" |
|
39 | decode "&" = "&" |
|
40 | decode "'" = "'" |
|
41 | decode """ = "\"" |
|
42 | decode c = c; |
|
43 |
|
44 val text = Library.translate_string encode; |
49 val text = Library.translate_string encode; |
45 |
50 |
46 val cdata_open = "<![CDATA[" |
51 val cdata = enclose "<![CDATA[" "]]>"; |
47 val cdata_close = "]]>" |
|
48 |
|
49 fun cdata s = cdata_open ^ s ^ cdata_close; |
|
50 |
52 |
51 |
53 |
52 (* elements *) |
54 (* elements *) |
53 |
|
54 datatype tree = |
|
55 Elem of string * (string * string) list * tree list |
|
56 | Text of string; |
|
57 |
55 |
58 fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\""; |
56 fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\""; |
59 |
57 |
60 fun element name atts cs = |
58 fun element name atts cs = |
61 let val elem = space_implode " " (name :: map attribute atts) in |
59 let val elem = space_implode " " (name :: map attribute atts) in |
62 if null cs then enclose "<" "/>" elem |
60 if null cs then enclose "<" "/>" elem |
63 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
61 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
64 end; |
62 end; |
65 |
63 |
66 fun string_of_tree (Elem (name, atts, ts)) = |
|
67 element name atts (map string_of_tree ts) |
|
68 | string_of_tree (Text s) = s; |
|
69 |
|
70 val header = "<?xml version=\"1.0\"?>\n"; |
|
71 |
64 |
72 |
65 |
73 (* parser *) |
66 (** explicit XML trees **) |
|
67 |
|
68 datatype tree = |
|
69 Elem of string * (string * string) list * tree list |
|
70 | Text of string; |
|
71 |
|
72 fun string_of_tree tree = |
|
73 let |
|
74 fun string_of (Elem (name, atts, ts)) buf = |
|
75 let val buf' = |
|
76 buf |> Buffer.add "<" |
|
77 |> fold Buffer.add (separate " " (name :: map attribute atts)) |
|
78 in |
|
79 if null ts then |
|
80 buf' |> Buffer.add "/>" |
|
81 else |
|
82 buf' |> Buffer.add ">" |
|
83 |> fold string_of ts |
|
84 |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">" |
|
85 end |
|
86 | string_of (Text s) buf = Buffer.add (text s) buf; |
|
87 in Buffer.content (string_of tree Buffer.empty) end; |
|
88 |
|
89 |
|
90 |
|
91 (** XML parsing **) |
74 |
92 |
75 fun err s (xs, _) = |
93 fun err s (xs, _) = |
76 "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs); |
94 "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs); |
77 |
95 |
78 val scan_whspc = Scan.any Symbol.is_blank; |
96 val scan_whspc = Scan.any Symbol.is_blank; |