1.1 --- a/src/Pure/ProofGeneral/pgip_output.ML Mon Jan 22 15:36:58 2007 +0100
1.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML Mon Jan 22 15:37:08 2007 +0100
1.3 @@ -37,6 +37,12 @@
1.4 | Hasprefs of { prefcategory: string option,
1.5 prefs: PgipTypes.preference list }
1.6 | Prefval of { name: string, value: string }
1.7 + | Setrefs of { url: PgipTypes.pgipurl option,
1.8 + thyname: PgipTypes.objname option,
1.9 + objtype: PgipTypes.objtype option,
1.10 + name: PgipTypes.objname option,
1.11 + idtables: PgipTypes.idtable list,
1.12 + fileurls : PgipTypes.pgipurl list }
1.13 | Idvalue of { name: PgipTypes.objname,
1.14 objtype: PgipTypes.objtype,
1.15 text: XML.content }
1.16 @@ -87,6 +93,12 @@
1.17 | Idvalue of { name: PgipTypes.objname,
1.18 objtype: PgipTypes.objtype,
1.19 text: XML.content }
1.20 + | Setrefs of { url: PgipTypes.pgipurl option,
1.21 + thyname: PgipTypes.objname option,
1.22 + objtype: PgipTypes.objtype option,
1.23 + name: PgipTypes.objname option,
1.24 + idtables: PgipTypes.idtable list,
1.25 + fileurls : PgipTypes.pgipurl list }
1.26 | Informguise of { file : PgipTypes.pgipurl option,
1.27 theory: PgipTypes.objname option,
1.28 theorem: PgipTypes.objname option,
1.29 @@ -224,6 +236,25 @@
1.30 XML.Elem ("setids",[],map idtable_to_xml idtables)
1.31 end
1.32
1.33 +fun setrefs (Setrefs vs) =
1.34 + let
1.35 + val url = #url vs
1.36 + val thyname = #thyname vs
1.37 + val objtype = #objtype vs
1.38 + val name = #name vs
1.39 + val idtables = #idtables vs
1.40 + val fileurls = #fileurls vs
1.41 + fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
1.42 + in
1.43 + XML.Elem ("setrefs",
1.44 + (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @
1.45 + (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
1.46 + (opt_attr "thyname" thyname) @
1.47 + (opt_attr "name" name),
1.48 + (map idtable_to_xml idtables) @
1.49 + (map fileurl_to_xml fileurls))
1.50 + end
1.51 +
1.52 fun addids (Addids vs) =
1.53 let
1.54 val idtables = #idtables vs
1.55 @@ -356,6 +387,7 @@
1.56 | Lexicalstructure _ => lexicalstructure pgipoutput
1.57 | Proverinfo _ => proverinfo pgipoutput
1.58 | Setids _ => setids pgipoutput
1.59 + | Setrefs _ => setrefs pgipoutput
1.60 | Addids _ => addids pgipoutput
1.61 | Delids _ => delids pgipoutput
1.62 | Hasprefs _ => hasprefs pgipoutput