Huge reorganization of matita and ocaml.

[helm.git] / helm / ocaml / library / libraryClean.ml

diff --git a/helm/ocaml/library/libraryClean.ml b/helm/ocaml/library/libraryClean.ml
index 00f2c4ef0f168e13eecc6c49c701acd502974aae..5da9507fc6509f1e8cd2ca955047592362a93f01 100644 (file)
--- a/helm/ocaml/library/libraryClean.ml
+++ b/helm/ocaml/library/libraryClean.ml
@@ -145,7 +145,7 @@ let moo_root_dir = lazy (
   String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
 )
 
-let close_nodb buris =
+let close_nodb ~basedir buris =
   let rev_deps = Hashtbl.create 97 in
   let all_moos =
     HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
@@ -154,19 +154,17 @@ let close_nodb buris =
   List.iter
     (fun path -> 
       let metadata = LibraryNoDb.load_metadata ~fname:path in
-      let baseuri_of_current_moo = 
-        let rec aux = function 
-          | [] -> assert false
-          | LibraryNoDb.Baseuri buri::_ -> buri
-          | _ :: tl -> aux tl
-        in
-        aux metadata
+      let baseuri_of_current_moo =
+       let dirname = Filename.chop_extension (Filename.dirname path) in
+       let basedirlen = String.length basedir in
+        assert (String.sub dirname 0 basedirlen = basedir);
+        "cic:" ^
+        String.sub dirname basedirlen (String.length dirname - basedirlen) ^
+         Filename.basename path
       in
       let deps = 
         HExtlib.filter_map 
-          (function 
-          | LibraryNoDb.Dependency buri -> Some buri
-          | _ -> None ) 
+          (function LibraryNoDb.Dependency buri -> Some buri)
         metadata
       in
       List.iter 
@@ -198,7 +196,7 @@ let clean_baseuris ?(verbose=true) ~basedir buris =
     List.iter debug_prerr buris; 
   let l = 
     if Helm_registry.get_bool "db.nodb" then
-      close_nodb buris
+      close_nodb ~basedir buris
     else
       close_db [] buris 
   in
@@ -209,7 +207,9 @@ let clean_baseuris ?(verbose=true) ~basedir buris =
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
   List.iter
    (fun buri ->
-     HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri)) 
+     HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri);
+     HExtlib.safe_remove (LibraryMisc.metadata_file_of_baseuri basedir buri);
+     HExtlib.safe_remove (LibraryMisc.lexicon_file_of_baseuri basedir buri))
    (HExtlib.list_uniq (List.fast_sort Pervasives.compare
      (List.map (UriManager.buri_of_uri) l)));
   List.iter