(* $Id$ *)
+let object_declaration_hook = ref (fun _ _ -> ());;
+let set_object_declaration_hook f =
+ object_declaration_hook := f
+
exception AlreadyDefined of UriManager.uri
let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
HExtlib.mkdir dir
in
(* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj, innertypes =
+ let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
if Helm_registry.get_bool "matita.system" then
- let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
+ let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
Cic2acic.acic_object_of_cic_object obj
in
let innertypesxml =
Cic2Xml.print_inner_types
uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
in
- annobj, Some innertypesxml
+ annobj, Some innertypesxml, Some ids_to_inner_sorts, false
else
let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
- annobj, None
+ annobj, None, None, true
in
(* prepare XML *)
let xml, bodyxml =
Cic2Xml.print_object
- uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
+ uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+ ~generate_attributes annobj
in
let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
xmlunivgraphpath, univgraphuri =
try
(*3*)
let new_stuff = save_object_to_disk uri obj ugraph univlist in
+ (* EXPERIMENTAL: pretty print the object in natural language *)
+ (try !object_declaration_hook uri obj
+ with exc ->
+ prerr_endline "Error: object_declaration_hook failed");
try
HLog.message
(Printf.sprintf "%s defined" (UriManager.string_of_uri uri))