author | wenzelm |
Fri, 17 Dec 2010 20:21:35 +0100 | |
changeset 41253 | 42f24340ae53 |
parent 38269 | cd6906d9199f |
child 43698 | 91c4d7397f0e |
permissions | -rw-r--r-- |
38266 | 1 |
(* Title: Pure/General/xml_data.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
XML as basic data representation language. |
|
5 |
*) |
|
6 |
||
7 |
signature XML_DATA = |
|
8 |
sig |
|
9 |
exception XML_ATOM of string |
|
10 |
exception XML_BODY of XML.body |
|
11 |
val make_properties: Properties.T -> XML.body |
|
12 |
val dest_properties: XML.body -> Properties.T |
|
13 |
val make_string: string -> XML.body |
|
14 |
val dest_string : XML.body -> string |
|
15 |
val make_int: int -> XML.body |
|
16 |
val dest_int : XML.body -> int |
|
17 |
val make_bool: bool -> XML.body |
|
18 |
val dest_bool: XML.body -> bool |
|
19 |
val make_unit: unit -> XML.body |
|
20 |
val dest_unit: XML.body -> unit |
|
21 |
val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body |
|
22 |
val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b |
|
23 |
val make_triple: |
|
24 |
('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body |
|
25 |
val dest_triple: |
|
26 |
(XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c |
|
27 |
val make_list: ('a -> XML.body) -> 'a list -> XML.body |
|
28 |
val dest_list: (XML.body -> 'a) -> XML.body -> 'a list |
|
29 |
val make_option: ('a -> XML.body) -> 'a option -> XML.body |
|
30 |
val dest_option: (XML.body -> 'a) -> XML.body -> 'a option |
|
31 |
end; |
|
32 |
||
33 |
structure XML_Data: XML_DATA = |
|
34 |
struct |
|
35 |
||
36 |
(* basic values *) |
|
37 |
||
38 |
exception XML_ATOM of string; |
|
39 |
||
40 |
||
41 |
fun make_int_atom i = signed_string_of_int i; |
|
42 |
||
43 |
fun dest_int_atom s = |
|
44 |
(case Int.fromString s of |
|
45 |
SOME i => i |
|
46 |
| NONE => raise XML_ATOM s); |
|
47 |
||
48 |
||
49 |
fun make_bool_atom false = "0" |
|
50 |
| make_bool_atom true = "1"; |
|
51 |
||
52 |
fun dest_bool_atom "0" = false |
|
53 |
| dest_bool_atom "1" = true |
|
54 |
| dest_bool_atom s = raise XML_ATOM s; |
|
55 |
||
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
38266
diff
changeset
|
56 |
|
38266 | 57 |
fun make_unit_atom () = ""; |
58 |
||
59 |
fun dest_unit_atom "" = () |
|
60 |
| dest_unit_atom s = raise XML_ATOM s; |
|
61 |
||
62 |
||
63 |
(* structural nodes *) |
|
64 |
||
65 |
exception XML_BODY of XML.tree list; |
|
66 |
||
67 |
fun make_node ts = XML.Elem ((":", []), ts); |
|
68 |
||
69 |
fun dest_node (XML.Elem ((":", []), ts)) = ts |
|
70 |
| dest_node t = raise XML_BODY [t]; |
|
71 |
||
72 |
||
73 |
(* representation of standard types *) |
|
74 |
||
75 |
fun make_properties props = [XML.Elem ((":", props), [])]; |
|
76 |
||
77 |
fun dest_properties [XML.Elem ((":", props), [])] = props |
|
78 |
| dest_properties ts = raise XML_BODY ts; |
|
79 |
||
80 |
||
38269 | 81 |
fun make_string "" = [] |
82 |
| make_string s = [XML.Text s]; |
|
38266 | 83 |
|
38269 | 84 |
fun dest_string [] = "" |
85 |
| dest_string [XML.Text s] = s |
|
38266 | 86 |
| dest_string ts = raise XML_BODY ts; |
87 |
||
88 |
||
89 |
val make_int = make_string o make_int_atom; |
|
90 |
val dest_int = dest_int_atom o dest_string; |
|
91 |
||
92 |
val make_bool = make_string o make_bool_atom; |
|
93 |
val dest_bool = dest_bool_atom o dest_string; |
|
94 |
||
95 |
val make_unit = make_string o make_unit_atom; |
|
96 |
val dest_unit = dest_unit_atom o dest_string; |
|
97 |
||
98 |
||
99 |
fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)]; |
|
100 |
||
101 |
fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2)) |
|
102 |
| dest_pair _ _ ts = raise XML_BODY ts; |
|
103 |
||
104 |
||
105 |
fun make_triple make1 make2 make3 (x, y, z) = |
|
106 |
[make_node (make1 x), make_node (make2 y), make_node (make3 z)]; |
|
107 |
||
108 |
fun dest_triple dest1 dest2 dest3 [t1, t2, t3] = |
|
109 |
(dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3)) |
|
110 |
| dest_triple _ _ _ ts = raise XML_BODY ts; |
|
111 |
||
112 |
||
113 |
fun make_list make xs = map (make_node o make) xs; |
|
114 |
||
115 |
fun dest_list dest ts = map (dest o dest_node) ts; |
|
116 |
||
117 |
||
118 |
fun make_option make NONE = make_list make [] |
|
119 |
| make_option make (SOME x) = make_list make [x]; |
|
120 |
||
121 |
fun dest_option dest ts = |
|
122 |
(case dest_list dest ts of |
|
123 |
[] => NONE |
|
124 |
| [x] => SOME x |
|
125 |
| _ => raise XML_BODY ts); |
|
126 |
||
127 |
end; |
|
128 |