X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FlibraryClean.ml;h=6f72ff495b77edf2389397863bf56bd7de3778b3;hb=5976abe5d66b4e52db76e8de10e9de6829349e44;hp=f2ac571995c8552d18fa6eeef474153b081cbca0;hpb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;p=helm.git

diff --git a/helm/ocaml/library/libraryClean.ml b/helm/ocaml/library/libraryClean.ml
index f2ac57199..6f72ff495 100644
--- a/helm/ocaml/library/libraryClean.ml
+++ b/helm/ocaml/library/libraryClean.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 let debug = false
@@ -30,9 +32,7 @@ let debug_prerr = if debug then prerr_endline else ignore
 
 module HGT = Http_getter_types;;
 module HG = Http_getter;;
-module HGM = Http_getter_misc;;
 module UM = UriManager;;
-module TA = GrafiteAst;;
 
 let cache_of_processed_baseuri = Hashtbl.create 1024
 
@@ -124,10 +124,10 @@ let close_uri_list uri_to_remove =
   in
   uri_to_remove, depend
 
-let rec close_using_db uris next =
+let rec close_db uris next =
   match next with
   | [] -> uris
-  | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
+  | l -> let uris, next = close_uri_list l in close_db uris next @ uris
   
 let cleaned_no = ref 0;;
 
@@ -140,40 +140,38 @@ let moo_root_dir = lazy (
           match
             Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
           with
-          | [a;b] -> a, b
+          | a::b::_ -> a, b
           | _ -> assert false)
         (Helm_registry.get_list Helm_registry.string "getter.prefix"))
   in
   String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
 )
 
-let close_using_moos 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")
+  let all_metadata =
+    HExtlib.find ~test:(fun name -> Filename.check_suffix name ".metadata")
       (Lazy.force moo_root_dir)
   in
   List.iter
     (fun path -> 
-      let _, metadata = GrafiteMarshal.load_moo ~fname:path in
-      let baseuri_of_current_moo = 
-        let rec aux = function 
-          | [] -> assert false
-          | GrafiteAst.Baseuri buri::_ -> buri
-          | _ :: tl -> aux tl
-        in
-        aux metadata
+      let metadata = LibraryNoDb.load_metadata ~fname:path in
+      let baseuri_of_current_metadata =
+       let dirname = 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 
-          | GrafiteAst.Dependency buri -> Some buri
-          | _ -> None ) 
+          (function LibraryNoDb.Dependency buri -> Some buri)
         metadata
       in
       List.iter 
-        (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
-  all_moos;
+        (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_metadata) deps)
+    all_metadata;
   let buris_to_remove = 
     HExtlib.list_uniq  
       (List.fast_sort Pervasives.compare 
@@ -194,15 +192,15 @@ let close_using_moos buris =
 
 let clean_baseuris ?(verbose=true) ~basedir buris =
   Hashtbl.clear cache_of_processed_baseuri;
-  let buris = List.map HGM.strip_trailing_slash buris in
+  let buris = List.map Http_getter_misc.strip_trailing_slash buris in
   debug_prerr "clean_baseuris called on:";
   if debug then
     List.iter debug_prerr buris; 
   let l = 
     if Helm_registry.get_bool "db.nodb" then
-      close_using_moos buris
+      close_nodb ~basedir buris
     else
-      close_using_db [] buris 
+      close_db [] buris 
   in
   let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in
@@ -211,7 +209,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