remove_obj is now much faster:

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 9529375ae57a6b36c3317c45b8878ff24fa6932e..a3429840b7b2e169c835c753529de9e4cabed0e3 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -157,22 +157,24 @@ let remove_single_obj uri =
    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
   in
-  let to_remove =
-    uri :: 
-    (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
-    derived_uris_of_uri uri
-  in   
+  let uris_to_remove =
+   if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
+  in
+  let files_to_remove = uri :: derived_uris_of_uri uri in   
+  List.iter 
+   (fun uri -> 
+     (try
+       let file = Http_getter.resolve' ~writable:true uri in
+        HExtlib.safe_remove file;
+        HExtlib.rmdir_descend (Filename.dirname file)
+     with Http_getter_types.Key_not_found _ -> ());
+   ) files_to_remove ;
   List.iter 
-    (fun uri -> 
-      (try
-        let file = Http_getter.resolve' ~writable:true uri in
-         HExtlib.safe_remove file;
-         HExtlib.rmdir_descend (Filename.dirname file)
-      with Http_getter_types.Key_not_found _ -> ());
-      ignore (LibraryDb.remove_uri uri);
-      (*CoercGraph.remove_coercion uri;*)
-      CicEnvironment.remove_obj uri)
-  to_remove
+   (fun uri -> 
+     ignore (LibraryDb.remove_uri uri);
+     (*CoercGraph.remove_coercion uri;*)
+     CicEnvironment.remove_obj uri
+   ) uris_to_remove
 
 (*** GENERATION OF AUXILIARY LEMMAS ***)