NG decompilation is now activated. However, it is called from the old

decompilation that cannot detect when a NG-only file A is used by another
NG-only file B. As a consequence, decompiling A does not decompile B too.

diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml
index 9a3b172454c00268bd0a4320030bee9711b76a6a..8e9f430ba7ee467969ebe947b5142b1fc73d4804 100644 (file)
--- a/helm/software/components/library/libraryClean.ml
+++ b/helm/software/components/library/libraryClean.ml
@@ -34,6 +34,8 @@ module HGT = Http_getter_types;;
 module HG = Http_getter;;
 module UM = UriManager;;
 
+let decompile = ref (fun ~baseuri -> assert false);;
+let set_decompile_cb f = decompile := f;;
 
 let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;;
 
@@ -230,6 +232,7 @@ let clean_baseuris ?(verbose=true) buris =
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
   List.iter
    (fun baseuri ->
+     !decompile ~baseuri;
      try 
       let obj_file =
        LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri

diff --git a/helm/software/components/library/libraryClean.mli b/helm/software/components/library/libraryClean.mli
index 4d65cfe38daa87a7bc9f5d8de0f653e5b23b3a0f..89f3b7b1dbf066cec84965f039cdab681ee42f13 100644 (file)
--- a/helm/software/components/library/libraryClean.mli
+++ b/helm/software/components/library/libraryClean.mli
@@ -23,5 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
+val set_decompile_cb: (baseuri: string -> unit) -> unit
+
 val db_uris_of_baseuri : string -> string list
 val clean_baseuris : ?verbose:bool -> string list -> unit

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index 47c8d67c6d4251ec5a0df01c106baf678a651545..18b7903e55d4ad66762491a72f45333d445ec546 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -38,13 +38,16 @@ let time_travel status =
   storage := sto; aliases := ali; cache := cac
 ;;
 
-let path_of_baseuri baseuri =
+let path_of_baseuri ?(no_suffix=false) baseuri =
  let uri = NUri.string_of_uri baseuri in
  let path = String.sub uri 4 (String.length uri - 4) in
  let path = Helm_registry.get "matita.basedir" ^ path in
  let dirname = Filename.dirname path in
   HExtlib.mkdir dirname;
-  path ^ ".ng"
+  if no_suffix then
+   path
+  else
+   path ^ ".ng"
 ;;
 
 let magic = 0;;
@@ -127,10 +130,27 @@ module Serializer(S: sig type status end) =
 end
 
 let decompile ~baseuri =
- Unix.unlink (path_of_baseuri baseuri)
- (* WE ARE NOT REMOVING ALL THE OBJECTS YET! *)
+ HExtlib.safe_remove (path_of_baseuri baseuri);
+ let basepath = path_of_baseuri ~no_suffix:true baseuri in
+ try
+  let od = Unix.opendir basepath in
+  let rec aux names =
+   try
+    let name = Unix.readdir od in
+     if name <> "." && name <> ".." then aux (name::names) else aux names
+   with
+    End_of_file -> names in
+  let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in
+   Unix.closedir od;
+   List.iter Unix.unlink names;
+   HExtlib.rmdir_descend basepath
+ with
+  Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *)
 ;;
 
+LibraryClean.set_decompile_cb
+ (fun ~baseuri -> decompile ~baseuri:(NUri.uri_of_string baseuri));;
+
 let fetch_obj uri =
  let obj = require0 ~baseuri:uri in
   refresh_uri_in_obj obj