-let paths_and_uris_of_obj uri status =
- let basedir = get_string_option status "basedir" in
- let innertypesuri = UriManager.innertypesuri_of_uri uri in
- let bodyuri = UriManager.bodyuri_of_uri uri in
- let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
- (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
- let innertypespath = basedir ^ "/" ^ innertypesfilename in
- let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri uri) ^ ".xml.gz" in
- let xmlpath = basedir ^ "/" ^ xmlfilename in
- let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
- let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in
- xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
-
-let save_object_to_disk status uri obj =
- let ensure_path_exists path =
- let dir = Filename.dirname path in
- MatitaMisc.mkdir dir
- in
- (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
- Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
- in
- (* prepare XML *)
- let xml, bodyxml =
- Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
- annobj
- in
- let xmlinnertypes =
- Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
- ~ask_dtd_to_the_getter:false
- in
- let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri =
- paths_and_uris_of_obj uri status
- in
- let path_scheme_of path = "file://" ^ path in
- List.iter MatitaMisc.mkdir
- (List.map Filename.dirname [innertypespath; xmlpath]);
- (* now write to disk *)
- ensure_path_exists innertypespath;
- Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
- ensure_path_exists xmlpath;
- Xml.pp ~gzip:true xml (Some xmlpath) ;
- (* now register to the getter *)
- Http_getter.register' innertypesuri (path_scheme_of innertypespath);
- Http_getter.register' uri (path_scheme_of xmlpath);
- (* we return a list of uri,path we registered/created *)
- (uri,xmlpath) :: (innertypesuri,innertypespath) ::
- (* now the optional body, both write and register *)
- (match bodyxml,bodyuri with
- None,None -> []
- | Some bodyxml,Some bodyuri->
- ensure_path_exists xmlbodypath;
- Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
- Http_getter.register' bodyuri (path_scheme_of xmlbodypath);
- [bodyuri,xmlbodypath]
- | _-> assert false)