src/Pure/ProofGeneral/pgip_output.ML
changeset 22161 b2117f4f2d39
parent 22040 635aaa46b44d
child 22336 050ceb649207
     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