16 datatype pgmlplace = Subscript | Superscript | Above | Below |
16 datatype pgmlplace = Subscript | Superscript | Above | Below |
17 |
17 |
18 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
18 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
19 |
19 |
20 datatype pgmlaction = Toggle | Button | Menu |
20 datatype pgmlaction = Toggle | Button | Menu |
21 |
21 |
22 datatype pgmlterm = |
22 datatype pgmlterm = |
23 Atoms of { kind: string option, content: pgmlatom list } |
23 Atoms of { kind: string option, content: pgmlatom list } |
24 | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list } |
24 | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list } |
25 | Break of { mandatory: bool option, indent: int option } |
25 | Break of { mandatory: bool option, indent: int option } |
26 | Subterm of { kind: string option, |
26 | Subterm of { kind: string option, |
27 param: string option, |
27 param: string option, |
28 place: pgmlplace option, |
28 place: pgmlplace option, |
29 name: string option, |
29 name: string option, |
30 decoration: pgmldec option, |
30 decoration: pgmldec option, |
31 action: pgmlaction option, |
31 action: pgmlaction option, |
32 pos: string option, |
32 pos: string option, |
33 xref: PgipTypes.pgipurl option, |
33 xref: PgipTypes.pgipurl option, |
34 content: pgmlterm list } |
34 content: pgmlterm list } |
35 | Alt of { kind: string option, content: pgmlterm list } |
35 | Alt of { kind: string option, content: pgmlterm list } |
36 | Embed of XML.tree list |
36 | Embed of XML.tree list |
37 | Raw of XML.tree |
37 | Raw of XML.tree |
38 |
38 |
39 datatype pgml = |
39 datatype pgml = |
40 Pgml of { version: string option, systemid: string option, |
40 Pgml of { version: string option, systemid: string option, |
41 area: PgipTypes.displayarea option, |
41 area: PgipTypes.displayarea option, |
42 content: pgmlterm list } |
42 content: pgmlterm list } |
43 |
43 |
44 val pgmlterm_to_xml : pgmlterm -> XML.tree |
44 val pgmlterm_to_xml : pgmlterm -> XML.tree |
45 |
45 |
46 val pgml_to_xml : pgml -> XML.tree |
46 val pgml_to_xml : pgml -> XML.tree |
47 end |
47 end |
48 |
48 |
60 datatype pgmlplace = Subscript | Superscript | Above | Below |
60 datatype pgmlplace = Subscript | Superscript | Above | Below |
61 |
61 |
62 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
62 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
63 |
63 |
64 datatype pgmlaction = Toggle | Button | Menu |
64 datatype pgmlaction = Toggle | Button | Menu |
65 |
65 |
66 datatype pgmlterm = |
66 datatype pgmlterm = |
67 Atoms of { kind: string option, content: pgmlatom list } |
67 Atoms of { kind: string option, content: pgmlatom list } |
68 | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list } |
68 | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list } |
69 | Break of { mandatory: bool option, indent: int option } |
69 | Break of { mandatory: bool option, indent: int option } |
70 | Subterm of { kind: string option, |
70 | Subterm of { kind: string option, |
71 param: string option, |
71 param: string option, |
72 place: pgmlplace option, |
72 place: pgmlplace option, |
73 name: string option, |
73 name: string option, |
74 decoration: pgmldec option, |
74 decoration: pgmldec option, |
75 action: pgmlaction option, |
75 action: pgmlaction option, |
76 pos: string option, |
76 pos: string option, |
77 xref: PgipTypes.pgipurl option, |
77 xref: PgipTypes.pgipurl option, |
78 content: pgmlterm list } |
78 content: pgmlterm list } |
79 | Alt of { kind: string option, content: pgmlterm list } |
79 | Alt of { kind: string option, content: pgmlterm list } |
80 | Embed of XML.tree list |
80 | Embed of XML.tree list |
81 | Raw of XML.tree |
81 | Raw of XML.tree |
82 |
82 |
83 |
83 |
84 datatype pgml = |
84 datatype pgml = |
85 Pgml of { version: string option, systemid: string option, |
85 Pgml of { version: string option, systemid: string option, |
86 area: PgipTypes.displayarea option, |
86 area: PgipTypes.displayarea option, |
87 content: pgmlterm list } |
87 content: pgmlterm list } |
88 |
88 |
89 fun pgmlorient_to_string HOVOrient = "hov" |
89 fun pgmlorient_to_string HOVOrient = "hov" |
90 | pgmlorient_to_string HOrient = "h" |
90 | pgmlorient_to_string HOrient = "h" |
91 | pgmlorient_to_string VOrient = "v" |
91 | pgmlorient_to_string VOrient = "v" |
92 | pgmlorient_to_string HVOrient = "hv" |
92 | pgmlorient_to_string HVOrient = "hv" |
109 |
109 |
110 (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; |
110 (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; |
111 would be better not to *) |
111 would be better not to *) |
112 fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content]) |
112 fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content]) |
113 | atom_to_xml (Str str) = XML.Output str |
113 | atom_to_xml (Str str) = XML.Output str |
114 |
114 |
115 fun pgmlterm_to_xml (Atoms {kind, content}) = |
115 fun pgmlterm_to_xml (Atoms {kind, content}) = |
116 XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content) |
116 XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content) |
117 |
117 |
118 | pgmlterm_to_xml (Box {orient, indent, content}) = |
118 | pgmlterm_to_xml (Box {orient, indent, content}) = |
119 XML.Elem("box", |
119 XML.Elem("box", |
120 opt_attr_map pgmlorient_to_string "orient" orient @ |
120 opt_attr_map pgmlorient_to_string "orient" orient @ |
121 opt_attr_map int_to_pgstring "indent" indent, |
121 opt_attr_map int_to_pgstring "indent" indent, |
122 map pgmlterm_to_xml content) |
122 map pgmlterm_to_xml content) |
123 |
123 |
124 | pgmlterm_to_xml (Break {mandatory, indent}) = |
124 | pgmlterm_to_xml (Break {mandatory, indent}) = |
125 XML.Elem("break", |
125 XML.Elem("break", |
126 opt_attr_map bool_to_pgstring "mandatory" mandatory @ |
126 opt_attr_map bool_to_pgstring "mandatory" mandatory @ |
127 opt_attr_map int_to_pgstring "indent" indent, []) |
127 opt_attr_map int_to_pgstring "indent" indent, []) |
128 |
128 |
129 | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) = |
129 | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) = |
130 XML.Elem("subterm", |
130 XML.Elem("subterm", |
131 opt_attr "kind" kind @ |
131 opt_attr "kind" kind @ |
132 opt_attr "param" param @ |
132 opt_attr "param" param @ |
133 opt_attr_map pgmlplace_to_string "place" place @ |
133 opt_attr_map pgmlplace_to_string "place" place @ |
134 opt_attr "name" name @ |
134 opt_attr "name" name @ |
135 opt_attr_map pgmldec_to_string "decoration" decoration @ |
135 opt_attr_map pgmldec_to_string "decoration" decoration @ |
136 opt_attr_map pgmlaction_to_string "action" action @ |
136 opt_attr_map pgmlaction_to_string "action" action @ |
137 opt_attr "pos" pos @ |
137 opt_attr "pos" pos @ |
138 opt_attr_map string_of_pgipurl "xref" xref, |
138 opt_attr_map string_of_pgipurl "xref" xref, |
139 map pgmlterm_to_xml content) |
139 map pgmlterm_to_xml content) |
140 |
140 |
141 | pgmlterm_to_xml (Alt {kind, content}) = |
141 | pgmlterm_to_xml (Alt {kind, content}) = |
142 XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content) |
142 XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content) |
143 |
143 |
144 | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls) |
144 | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls) |
145 |
145 |
146 | pgmlterm_to_xml (Raw xml) = xml |
146 | pgmlterm_to_xml (Raw xml) = xml |
147 |
147 |
148 |
148 |
149 datatype pgml = |
149 datatype pgml = |
150 Pgml of { version: string option, systemid: string option, |
150 Pgml of { version: string option, systemid: string option, |
151 area: PgipTypes.displayarea option, |
151 area: PgipTypes.displayarea option, |
152 content: pgmlterm list } |
152 content: pgmlterm list } |
153 |
153 |
154 fun pgml_to_xml (Pgml {version,systemid,area,content}) = |
154 fun pgml_to_xml (Pgml {version,systemid,area,content}) = |
155 XML.Elem("pgml", |
155 XML.Elem("pgml", |
156 opt_attr "version" version @ |
156 opt_attr "version" version @ |
157 opt_attr "systemid" systemid @ |
157 opt_attr "systemid" systemid @ |
158 Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]), |
158 Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]), |
159 map pgmlterm_to_xml content) |
159 map pgmlterm_to_xml content) |
160 end |
160 end |