innertypesuri,bodyuri,univgraphuri
let paths_and_uris_of_obj uri =
- let resolved = Http_getter.filename' ~writable:true uri in
+ let resolved = Http_getter.filename' ~local:true ~writable:true uri in
let basepath = Filename.dirname resolved in
let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
HExtlib.mkdir dir
in
(* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
+ let annobj, innertypes =
+ if Helm_registry.get_bool "matita.system" then
+ 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
+ else
+ let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
+ annobj, None
+ in
(* prepare XML *)
let xml, bodyxml =
Cic2Xml.print_object
uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
- in
+ in
let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
xmlunivgraphpath, univgraphuri =
paths_and_uris_of_obj uri
(* we return a list of uri,path we registered/created *)
(uri,xmlpath) ::
(univgraphuri,xmlunivgraphpath) ::
+ (* now the optional inner types, both write and register *)
+ (match innertypes with
+ | None -> []
+ | Some innertypesxml ->
+ write ensure_path_exists innertypespath;
+ write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
+ [innertypesuri, innertypespath]
+ ) @
(* now the optional body, both write and register *)
(match bodyxml,bodyuri with
None,_ -> []
raise exc
with exc ->
CicEnvironment.remove_obj uri; (* -1 *)
- raise exc
+ raise exc
end
let remove_single_obj uri =
List.iter
(fun uri ->
(try
- let file = Http_getter.resolve' ~writable:true uri in
+ let file = Http_getter.resolve' ~local:true ~writable:true uri in
HExtlib.safe_remove file;
HExtlib.rmdir_descend (Filename.dirname file)
with Http_getter_types.Key_not_found _ -> ());
(CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
else
let new_coercions =
- CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ CicCoercion.close_coercion_graph src_carr tgt_carr uri
baseuri
in
let new_coercions =
let add_obj refinement_toolkit uri obj =
add_single_obj uri obj refinement_toolkit;
let uris = ref [] in
+ let not_debug = not (Helm_registry.get_bool "matita.debug") in
try
begin
match obj with
end;
UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
!uris
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
+ with
+ | exn when not_debug ->
+ List.iter remove_single_obj !uris;
+ raise exn
let remove_obj uri =
let uris =