completed support for "-nodb", now also matitaclean and its library work with that...

[helm.git] / helm / matita / matitacleanLib.ml

diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index 2d1cbfdef4fb1d7a39cf9649b9f10c0fcec85c99..e8a1fd29a301bf1141f4ae2739929664aa2f9426 100644 (file)
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -52,7 +52,8 @@ let one_step_depend suri =
         let buri = HMysql.escape buri in
         let obj_tbl = MetadataTypes.obj_tbl () in
         sprintf 
-          "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'"
+        ("SELECT source, h_occurrence FROM %s WHERE " ^^ 
+         "h_occurrence REGEXP '^%s[^/]*$'")
             obj_tbl buri
       in
       try 
@@ -123,29 +124,96 @@ let close_uri_list uri_to_remove =
   in
   uri_to_remove, depend
 
-let rec close uris next =
+let rec close_using_db uris next =
   match next with
   | [] -> uris
-  | l -> let uris, next = close_uri_list l in close uris next @ uris
+  | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
   
 let cleaned_no = ref 0;;
 
+  (** TODO repellent code ... *)
+let moo_root_dir = lazy (
+  let url =
+    List.assoc "cic:/matita/"
+      (List.map
+        (fun pair ->
+          match
+            Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
+          with
+          | [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 rev_deps = Hashtbl.create 97 in
+  let all_moos =
+    HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
+      (Lazy.force moo_root_dir)
+  in
+  List.iter
+    (fun path -> 
+      let _, metadata = MatitaMoo.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
+      in
+      let deps = 
+        HExtlib.filter_map 
+          (function 
+          | GrafiteAst.Dependency buri -> Some buri
+          | _ -> None ) 
+        metadata
+      in
+      List.iter 
+        (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
+  all_moos;
+  let buris_to_remove = 
+    HExtlib.list_uniq  
+      (List.fast_sort Pervasives.compare 
+        (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
+  in
+  let objects_to_remove = 
+    let objs_of_buri buri =
+      HExtlib.filter_map 
+        (function 
+        | Http_getter_types.Ls_object o ->
+            Some (buri ^ "/" ^ o.Http_getter_types.uri)
+        | _ -> None) 
+      (Http_getter.ls buri)
+    in
+    List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
+  in
+  objects_to_remove
+
 let clean_baseuris ?(verbose=true) buris =
   Hashtbl.clear cache_of_processed_baseuri;
   let buris = List.map HGM.strip_trailing_slash buris in
   debug_prerr "clean_baseuris called on:";
   if debug then
     List.iter debug_prerr buris; 
-  let l = close [] buris in
+  let l = 
+    if Helm_registry.get_bool "db.nodb" then
+      close_using_moos buris
+    else
+      close_using_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
   debug_prerr "clean_baseuri will remove:";
   if debug then
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
-  Hashtbl.iter
-   (fun buri _ ->
+  List.iter
+   (fun buri ->
      MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) 
-   cache_of_processed_baseuri;
+   (HExtlib.list_uniq (List.fast_sort Pervasives.compare
+     (List.map (UriManager.buri_of_uri) l)));
   List.iter (MatitaSync.remove ~verbose) l;
   cleaned_no := !cleaned_no + List.length l;
   if !cleaned_no > 30 then