41 thyname: PgipTypes.objname option, |
41 thyname: PgipTypes.objname option, |
42 objtype: PgipTypes.objtype option, |
42 objtype: PgipTypes.objtype option, |
43 name: PgipTypes.objname option, |
43 name: PgipTypes.objname option, |
44 idtables: PgipTypes.idtable list, |
44 idtables: PgipTypes.idtable list, |
45 fileurls : PgipTypes.pgipurl list } |
45 fileurls : PgipTypes.pgipurl list } |
46 | Idvalue of { name: PgipTypes.objname, |
46 | Idvalue of { thyname: PgipTypes.objname option, |
47 objtype: PgipTypes.objtype, |
47 objtype: PgipTypes.objtype, |
|
48 name: PgipTypes.objname, |
48 text: XML.content } |
49 text: XML.content } |
49 | Informguise of { file : PgipTypes.pgipurl option, |
50 | Informguise of { file : PgipTypes.pgipurl option, |
50 theory: PgipTypes.objname option, |
51 theory: PgipTypes.objname option, |
51 theorem: PgipTypes.objname option, |
52 theorem: PgipTypes.objname option, |
52 proofpos: int option } |
53 proofpos: int option } |
88 | Setids of { idtables: PgipTypes.idtable list } |
89 | Setids of { idtables: PgipTypes.idtable list } |
89 | Delids of { idtables: PgipTypes.idtable list } |
90 | Delids of { idtables: PgipTypes.idtable list } |
90 | Addids of { idtables: PgipTypes.idtable list } |
91 | Addids of { idtables: PgipTypes.idtable list } |
91 | Hasprefs of { prefcategory: string option, prefs: preference list } |
92 | Hasprefs of { prefcategory: string option, prefs: preference list } |
92 | Prefval of { name: string, value: string } |
93 | Prefval of { name: string, value: string } |
93 | Idvalue of { name: PgipTypes.objname, |
94 | Idvalue of { thyname: PgipTypes.objname option, |
94 objtype: PgipTypes.objtype, |
95 objtype: PgipTypes.objtype, |
|
96 name: PgipTypes.objname, |
95 text: XML.content } |
97 text: XML.content } |
96 | Setrefs of { url: PgipTypes.pgipurl option, |
98 | Setrefs of { url: PgipTypes.pgipurl option, |
97 thyname: PgipTypes.objname option, |
99 thyname: PgipTypes.objname option, |
98 objtype: PgipTypes.objtype option, |
100 objtype: PgipTypes.objtype option, |
99 name: PgipTypes.objname option, |
101 name: PgipTypes.objname option, |
285 XML.Elem("prefval", attr "name" name, [XML.Text value]) |
287 XML.Elem("prefval", attr "name" name, [XML.Text value]) |
286 end |
288 end |
287 |
289 |
288 fun idvalue (Idvalue vs) = |
290 fun idvalue (Idvalue vs) = |
289 let |
291 let |
|
292 val objtype_attrs = attrs_of_objtype (#objtype vs) |
|
293 val thyname = #thyname vs |
290 val name = #name vs |
294 val name = #name vs |
291 val objtype_attrs = attrs_of_objtype (#objtype vs) |
|
292 val text = #text vs |
295 val text = #text vs |
293 in |
296 in |
294 XML.Elem("idvalue", attr "name" name @ objtype_attrs, text) |
297 XML.Elem("idvalue", |
|
298 objtype_attrs @ |
|
299 (opt_attr "thyname" thyname) @ |
|
300 (attr "name" name), |
|
301 text) |
295 end |
302 end |
296 |
303 |
297 fun informguise (Informguise vs) = |
304 fun informguise (Informguise vs) = |
298 let |
305 let |
299 val file = #file vs |
306 val file = #file vs |