]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/libraryClean.ml
NG decompilation is now activated. However, it is called from the old
[helm.git] / helm / software / components / library / libraryClean.ml
index 9a3b172454c00268bd0a4320030bee9711b76a6a..8e9f430ba7ee467969ebe947b5142b1fc73d4804 100644 (file)
@@ -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