3 Author: Markus Wenzel, LMU Muenchen |
3 Author: Markus Wenzel, LMU Muenchen |
4 Stefan Berghofer, TU Muenchen |
4 Stefan Berghofer, TU Muenchen |
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 |
6 |
7 Basic support for XML input and output. |
7 Basic support for XML input and output. |
|
8 |
|
9 FIXME da: missing input raises FAIL (scan.ML), should give error message. |
8 *) |
10 *) |
9 |
11 |
10 signature XML = |
12 signature XML = |
11 sig |
13 sig |
12 datatype tree = |
14 datatype tree = |
13 Elem of string * (string * string) list * tree list |
15 Elem of string * (string * string) list * tree list |
14 | Text of string |
16 | Text of string |
15 val element: string -> (string * string) list -> string list -> string |
17 val element: string -> (string * string) list -> string list -> string |
16 val text: string -> string |
18 val text: string -> string |
|
19 val cdata: string -> string |
17 val header: string |
20 val header: string |
18 val string_of_tree: tree -> string |
21 val string_of_tree: tree -> string |
19 val tree_of_string: string -> tree |
22 val tree_of_string: string -> tree |
20 val parse_content: string list -> tree list * string list |
23 val parse_content: string list -> tree list * string list |
21 val parse_elem: string list -> tree * string list |
24 val parse_elem: string list -> tree * string list |
41 | decode """ = "\"" |
44 | decode """ = "\"" |
42 | decode c = c; |
45 | decode c = c; |
43 |
46 |
44 val text = String.translate (encode o String.str); |
47 val text = String.translate (encode o String.str); |
45 |
48 |
|
49 val cdata_open = "<![CDATA[" |
|
50 val cdata_close = "]]>" |
|
51 |
|
52 fun cdata s = cdata_open ^ s ^ cdata_close; |
46 |
53 |
47 (* elements *) |
54 (* elements *) |
48 |
55 |
49 datatype tree = |
56 datatype tree = |
50 Elem of string * (string * string) list * tree list |
57 Elem of string * (string * string) list * tree list |
51 | Text of string; |
58 | Text of string; |
52 |
59 |
53 fun attribute (a, x) = a ^ " = " ^ Library.quote (text x); |
60 fun attribute (a, x) = a ^ " = " ^ "\"" (text x) "\""; |
54 |
61 |
55 fun element name atts cs = |
62 fun element name atts cs = |
56 let val elem = space_implode " " (name :: map attribute atts) in |
63 let val elem = space_implode " " (name :: map attribute atts) in |
57 if null cs then enclose "<" "/>" elem |
64 if null cs then enclose "<" "/>" elem |
58 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
65 else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name |
68 (* parser *) |
75 (* parser *) |
69 |
76 |
70 fun err s (xs, _) = "XML parsing error: " ^ s ^ "\nfound:\n" ^ |
77 fun err s (xs, _) = "XML parsing error: " ^ s ^ "\nfound:\n" ^ |
71 implode (take (100, xs)); |
78 implode (take (100, xs)); |
72 |
79 |
73 val scan_whspc = Scan.repeat ($$ " " || $$ "\n"); |
80 val scan_whspc = Scan.repeat ($$ " " || $$ "\n" || $$ "\t"); |
74 |
81 |
75 val literal = Scan.literal o Scan.make_lexicon o single o explode; |
82 val literal = Scan.literal o Scan.make_lexicon o single o explode; |
76 |
83 |
77 val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode; |
84 val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode; |
78 |
85 |