30 | Addids of { idtables: PgipTypes.idtable list } |
30 | Addids of { idtables: PgipTypes.idtable list } |
31 | Hasprefs of { prefcategory: string option, |
31 | Hasprefs of { prefcategory: string option, |
32 prefs: PgipTypes.preference list } |
32 prefs: PgipTypes.preference list } |
33 | Prefval of { name: string, value: string } |
33 | Prefval of { name: string, value: string } |
34 | Setrefs of { url: PgipTypes.pgipurl option, |
34 | Setrefs of { url: PgipTypes.pgipurl option, |
35 thyname: PgipTypes.objname option, |
35 thyname: PgipTypes.objname option, |
36 objtype: PgipTypes.objtype option, |
36 objtype: PgipTypes.objtype option, |
37 name: PgipTypes.objname option, |
37 name: PgipTypes.objname option, |
38 idtables: PgipTypes.idtable list, |
38 idtables: PgipTypes.idtable list, |
39 fileurls : PgipTypes.pgipurl list } |
39 fileurls : PgipTypes.pgipurl list } |
40 | Idvalue of { thyname: PgipTypes.objname option, |
40 | Idvalue of { thyname: PgipTypes.objname option, |
41 objtype: PgipTypes.objtype, |
41 objtype: PgipTypes.objtype, |
42 name: PgipTypes.objname, |
42 name: PgipTypes.objname, |
43 text: XML.tree list } |
43 text: XML.tree list } |
44 | Informguise of { file : PgipTypes.pgipurl option, |
44 | Informguise of { file : PgipTypes.pgipurl option, |
45 theory: PgipTypes.objname option, |
45 theory: PgipTypes.objname option, |
46 theorem: PgipTypes.objname option, |
46 theorem: PgipTypes.objname option, |
47 proofpos: int option } |
47 proofpos: int option } |
48 | Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, |
48 | Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, |
49 errs: XML.tree list } (* errs to become PGML *) |
49 errs: XML.tree list } (* errs to become PGML *) |
50 | Usespgip of { version: string, |
50 | Usespgip of { version: string, |
51 pgipelems: (string * bool * string list) list } |
51 pgipelems: (string * bool * string list) list } |
52 | Usespgml of { version: string } |
52 | Usespgml of { version: string } |
53 | Pgip of { tag: string option, |
53 | Pgip of { tag: string option, |
54 class: string, |
54 class: string, |
65 structure PgipOutput : PGIPOUTPUT = |
65 structure PgipOutput : PGIPOUTPUT = |
66 struct |
66 struct |
67 open PgipTypes |
67 open PgipTypes |
68 |
68 |
69 datatype pgipoutput = |
69 datatype pgipoutput = |
70 Normalresponse of { content: XML.tree list } |
70 Normalresponse of { content: XML.tree list } |
71 | Errorresponse of { fatality: fatality, |
71 | Errorresponse of { fatality: fatality, |
72 location: location option, |
72 location: location option, |
73 content: XML.tree list } |
73 content: XML.tree list } |
74 | Informfileloaded of { url: Path.T, completed: bool } |
74 | Informfileloaded of { url: Path.T, completed: bool } |
75 | Informfileoutdated of { url: Path.T, completed: bool } |
75 | Informfileoutdated of { url: Path.T, completed: bool } |
76 | Informfileretracted of { url: Path.T, completed: bool } |
76 | Informfileretracted of { url: Path.T, completed: bool } |
77 | Metainforesponse of { attrs: XML.attributes, content: XML.tree list } |
77 | Metainforesponse of { attrs: XML.attributes, content: XML.tree list } |
78 | Lexicalstructure of { content: XML.tree list } |
78 | Lexicalstructure of { content: XML.tree list } |
82 | Delids of { idtables: PgipTypes.idtable list } |
82 | Delids of { idtables: PgipTypes.idtable list } |
83 | Addids of { idtables: PgipTypes.idtable list } |
83 | Addids of { idtables: PgipTypes.idtable list } |
84 | Hasprefs of { prefcategory: string option, prefs: preference list } |
84 | Hasprefs of { prefcategory: string option, prefs: preference list } |
85 | Prefval of { name: string, value: string } |
85 | Prefval of { name: string, value: string } |
86 | Idvalue of { thyname: PgipTypes.objname option, |
86 | Idvalue of { thyname: PgipTypes.objname option, |
87 objtype: PgipTypes.objtype, |
87 objtype: PgipTypes.objtype, |
88 name: PgipTypes.objname, |
88 name: PgipTypes.objname, |
89 text: XML.tree list } |
89 text: XML.tree list } |
90 | Setrefs of { url: PgipTypes.pgipurl option, |
90 | Setrefs of { url: PgipTypes.pgipurl option, |
91 thyname: PgipTypes.objname option, |
91 thyname: PgipTypes.objname option, |
92 objtype: PgipTypes.objtype option, |
92 objtype: PgipTypes.objtype option, |
93 name: PgipTypes.objname option, |
93 name: PgipTypes.objname option, |
94 idtables: PgipTypes.idtable list, |
94 idtables: PgipTypes.idtable list, |
95 fileurls : PgipTypes.pgipurl list } |
95 fileurls : PgipTypes.pgipurl list } |
96 | Informguise of { file : PgipTypes.pgipurl option, |
96 | Informguise of { file : PgipTypes.pgipurl option, |
97 theory: PgipTypes.objname option, |
97 theory: PgipTypes.objname option, |
98 theorem: PgipTypes.objname option, |
98 theorem: PgipTypes.objname option, |
99 proofpos: int option } |
99 proofpos: int option } |
100 | Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument, |
100 | Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument, |
101 errs: XML.tree list } (* errs to become PGML *) |
101 errs: XML.tree list } (* errs to become PGML *) |
102 | Usespgip of { version: string, |
102 | Usespgip of { version: string, |
103 pgipelems: (string * bool * string list) list } |
103 pgipelems: (string * bool * string list) list } |
104 | Usespgml of { version: string } |
104 | Usespgml of { version: string } |
105 | Pgip of { tag: string option, |
105 | Pgip of { tag: string option, |
106 class: string, |
106 class: string, |
139 let |
139 let |
140 val url = #url vs |
140 val url = #url vs |
141 val completed = #completed vs |
141 val completed = #completed vs |
142 in |
142 in |
143 XML.Elem ("informfileloaded", |
143 XML.Elem ("informfileloaded", |
144 attrs_of_pgipurl url @ |
144 attrs_of_pgipurl url @ |
145 (attr "completed" (PgipTypes.bool_to_pgstring completed)), |
145 (attr "completed" (PgipTypes.bool_to_pgstring completed)), |
146 []) |
146 []) |
147 end |
147 end |
148 |
148 |
149 fun informfileoutdated (Informfileoutdated vs) = |
149 fun informfileoutdated (Informfileoutdated vs) = |
150 let |
150 let |
151 val url = #url vs |
151 val url = #url vs |
152 val completed = #completed vs |
152 val completed = #completed vs |
153 in |
153 in |
154 XML.Elem ("informfileoutdated", |
154 XML.Elem ("informfileoutdated", |
155 attrs_of_pgipurl url @ |
155 attrs_of_pgipurl url @ |
156 (attr "completed" (PgipTypes.bool_to_pgstring completed)), |
156 (attr "completed" (PgipTypes.bool_to_pgstring completed)), |
157 []) |
157 []) |
158 end |
158 end |
159 |
159 |
160 fun informfileretracted (Informfileretracted vs) = |
160 fun informfileretracted (Informfileretracted vs) = |
161 let |
161 let |
162 val url = #url vs |
162 val url = #url vs |
163 val completed = #completed vs |
163 val completed = #completed vs |
164 in |
164 in |
165 XML.Elem ("informfileretracted", |
165 XML.Elem ("informfileretracted", |
166 attrs_of_pgipurl url @ |
166 attrs_of_pgipurl url @ |
167 (attr "completed" (PgipTypes.bool_to_pgstring completed)), |
167 (attr "completed" (PgipTypes.bool_to_pgstring completed)), |
168 []) |
168 []) |
169 end |
169 end |
170 |
170 |
171 fun metainforesponse (Metainforesponse vs) = |
171 fun metainforesponse (Metainforesponse vs) = |
172 let |
172 let |
173 val attrs = #attrs vs |
173 val attrs = #attrs vs |
209 XML.Elem ("setids",[],map idtable_to_xml idtables) |
209 XML.Elem ("setids",[],map idtable_to_xml idtables) |
210 end |
210 end |
211 |
211 |
212 fun setrefs (Setrefs vs) = |
212 fun setrefs (Setrefs vs) = |
213 let |
213 let |
214 val url = #url vs |
214 val url = #url vs |
215 val thyname = #thyname vs |
215 val thyname = #thyname vs |
216 val objtype = #objtype vs |
216 val objtype = #objtype vs |
217 val name = #name vs |
217 val name = #name vs |
218 val idtables = #idtables vs |
218 val idtables = #idtables vs |
219 val fileurls = #fileurls vs |
219 val fileurls = #fileurls vs |
220 fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, []) |
220 fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, []) |
221 in |
221 in |
222 XML.Elem ("setrefs", |
222 XML.Elem ("setrefs", |
223 (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @ |
223 (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @ |
224 (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @ |
224 (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @ |
225 (opt_attr "thyname" thyname) @ |
225 (opt_attr "thyname" thyname) @ |
226 (opt_attr "name" name), |
226 (opt_attr "name" name), |
227 (map idtable_to_xml idtables) @ |
227 (map idtable_to_xml idtables) @ |
228 (map fileurl_to_xml fileurls)) |
228 (map fileurl_to_xml fileurls)) |
229 end |
229 end |
230 |
230 |
231 fun addids (Addids vs) = |
231 fun addids (Addids vs) = |
232 let |
232 let |
233 val idtables = #idtables vs |
233 val idtables = #idtables vs |
258 XML.Elem("prefval", attr "name" name, [XML.Text value]) |
258 XML.Elem("prefval", attr "name" name, [XML.Text value]) |
259 end |
259 end |
260 |
260 |
261 fun idvalue (Idvalue vs) = |
261 fun idvalue (Idvalue vs) = |
262 let |
262 let |
263 val objtype_attrs = attrs_of_objtype (#objtype vs) |
263 val objtype_attrs = attrs_of_objtype (#objtype vs) |
264 val thyname = #thyname vs |
264 val thyname = #thyname vs |
265 val name = #name vs |
265 val name = #name vs |
266 val text = #text vs |
266 val text = #text vs |
267 in |
267 in |
268 XML.Elem("idvalue", |
268 XML.Elem("idvalue", |
269 objtype_attrs @ |
269 objtype_attrs @ |
270 (opt_attr "thyname" thyname) @ |
270 (opt_attr "thyname" thyname) @ |
271 (attr "name" name), |
271 (attr "name" name), |
272 text) |
272 text) |
273 end |
273 end |
274 |
274 |
275 fun informguise (Informguise vs) = |
275 fun informguise (Informguise vs) = |
276 let |
276 let |
277 val file = #file vs |
277 val file = #file vs |