From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 23 Jun 2009 10:23:59 +0000 (+0000)
Subject: - Bug fixed: removed URIs were not removed from the dependencies DB.
X-Git-Tag: make_still_working~3820
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=cf60cad5ad896f358d6e8dd2ded1c0430ba2c55c;p=helm.git

- Bug fixed: removed URIs were not removed from the dependencies DB.
- The assert failure has been removed since in some situations (????) an
  empty dir (no new objects) was not created and thus it was normal that it
  was not removed. TO BE BETTER UNDERSTOOD
---

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index da38ef0e1..98f8903d8 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -69,12 +69,12 @@ let local_aliases = ref [];;
 let cache = ref NUri.UriMap.empty;;
 let includes = ref [];;
 
-let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps =
+let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
  let global_aliases = ref [] in
- let includes_map = ref NUri.UriMap.empty in
+ let rev_includes_map = ref NUri.UriMap.empty in
  let store_db () =
   let ch = open_out (db_path ()) in
-  Marshal.to_channel ch (magic,(!global_aliases,!includes_map)) [];
+  Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) [];
   close_out ch in
  let load_db () =
   try
@@ -90,12 +90,12 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps =
      ) im NUri.UriMap.empty
    in
     global_aliases := ga;
-    includes_map := im
+    rev_includes_map := im
   with
    Sys_error _ -> () in
  let get_deps u =
   let get_deps_one_step u =
-    try NUri.UriMap.find u !includes_map with Not_found -> [] in
+    try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in
   let rec aux res =
    function
       [] -> res
@@ -105,15 +105,22 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps =
        else
         aux (he::res) (get_deps_one_step he @ tl)
   in
-   aux [] [u]
+   aux [] [u] in
+ let remove_deps u =
+  rev_includes_map := NUri.UriMap.remove u !rev_includes_map;
+  rev_includes_map :=
+   NUri.UriMap.map
+    (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map;
+  store_db ()
  in
   load_db,
   (fun ga -> global_aliases := ga; store_db ()),
   (fun () -> !global_aliases),
   (fun u l ->
-    includes_map := NUri.UriMap.add u (l @ get_deps u) !includes_map;
+    rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map;
     store_db ()),
-  get_deps
+  get_deps,
+  remove_deps
 ;;
 
 let init = load_db;;
@@ -190,6 +197,7 @@ end
 let decompile ~baseuri =
  let baseuris = get_deps baseuri in
  List.iter (fun baseuri ->
+  remove_deps baseuri;
   HExtlib.safe_remove (path_of_baseuri baseuri);
   let basepath = path_of_baseuri ~no_suffix:true baseuri in
   try
@@ -210,10 +218,7 @@ let decompile ~baseuri =
         Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri
       ) (get_global_aliases ()))
   with
-   Unix.Unix_error (_,m1,m2) -> (* raised by Unix.opendir, we hope :-) *)
-    if List.length baseuris <> 1 then
-     prerr_endline ("CRITICAL ERROR: " ^ m1 ^ ": " ^ m2);
-    assert (List.length baseuris = 1)
+   Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *)
  ) baseuris
 ;;