X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaSync.ml;h=f2c9d6e336858c9d236524a5752c81ce1f00ce09;hb=3147daf418c31528a67462c77b4cb3fd6431289c;hp=9a8cb10eee436997df984b100a3326befde2c65b;hpb=2eeeed0dca0fd4fde2c0ec2b98db40d327e7e158;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 9a8cb10ee..f2c9d6e33 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -125,7 +125,7 @@ let paths_and_uris_of_obj uri status =
 let save_object_to_disk status uri obj ugraph univlist =
   let ensure_path_exists path =
     let dir = Filename.dirname path in
-    MatitaMisc.mkdir dir
+    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 
@@ -139,14 +139,13 @@ let save_object_to_disk status uri obj ugraph univlist =
     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]);
+  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
   (* now write to disk *)
   ensure_path_exists xmlpath;
   Xml.pp ~gzip:true xml (Some xmlpath);
   CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
   (* we return a list of uri,path we registered/created *)
-  (uri,xmlpath) :: (innertypesuri,innertypespath) :: 
+  (uri,xmlpath) ::
   (univgraphuri,xmlunivgraphpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
@@ -307,7 +306,9 @@ let remove ?(verbose=false) uri =
             MatitaLog.debug ("Removing: " ^ baseuri ^ "/*");
             last_baseuri := baseuri
            end;
-        MatitaMisc.safe_remove (Http_getter.resolve' uri)
+           let file = Http_getter.resolve' uri in
+           MatitaMisc.safe_remove file;
+           MatitaMisc.rmdir_descend (Filename.dirname file)
       with Http_getter_types.Key_not_found _ -> ());
       remove_coercion uri; 
       ignore (MatitaDb.remove_uri uri);