aux
;;
-let xml_of_attrs attributes =
+let xml_of_attrs generate_attributes attributes =
let class_of = function
| `Coercion n ->
Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
List.fold_right
(fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
in
- Xml.xml_nempty "attributes" [] xml_attrs
+ if generate_attributes then Xml.xml_nempty "attributes" [] xml_attrs else [<>]
-let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+let print_object uri
+ ?ids_to_inner_sorts ?(generate_attributes=true) ~ask_dtd_to_the_getter obj =
let module C = Cic in
let module X = Xml in
let module U = UriManager in
match obj with
C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
- let xml_attrs = xml_of_attrs obj_attrs in
+ let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
let xml_for_current_proof_body =
(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
(*CSC: I think so. Not implemented yet. *)
xmlty, Some xmlbo
| C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
- let xml_attrs = xml_of_attrs obj_attrs in
+ let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
let xmlbo =
match bo with
None -> None
xmlty, xmlbo
| C.AVariable (id,n,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
- let xml_attrs = xml_of_attrs obj_attrs in
+ let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
let xmlbo =
match bo with
None -> [< >]
aobj, None
| C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
let params' = param_attribute_of_params params in
- let xml_attrs = xml_of_attrs obj_attrs in
+ let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;