- probe: critical bug fixed (all objects were deleted due to wrong test)

[helm.git] / matita / components / binaries / probe / matitaList.ml

diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml
index 7af98d59c8f92d3343d0a1146debebe3a16722e9..9f6248c0fcf39c4f540d291627eb3044624607d1 100644 (file)
--- a/matita/components/binaries/probe/matitaList.ml
+++ b/matita/components/binaries/probe/matitaList.ml
@@ -21,7 +21,12 @@ module US = U.UriSet
 module O = Options
 module E = Engine
 
-let src_exists path = !O.no_devel ||  Y.file_exists path
+let is_obj path = 
+   F.check_suffix path ".con.ng" ||
+   F.check_suffix path ".ind.ng" ||
+   F.check_suffix path ".var.ng"
+  
+let src_exists path = !O.no_devel || Y.file_exists path
 
 let mk_file path =
    if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
@@ -38,11 +43,15 @@ let add_src devel path =
       let str = F.concat "cic:" path ^ "/" in
       O.srcs := US.add (U.uri_of_string str) !O.srcs
 
+let add_remove base path =
+   O.remove := F.concat base path :: !O.remove
+
 let rec scan_entry base devel path =
-   if F.check_suffix path ".con.ng" then add_obj path else
-   if F.check_suffix path ".ind.ng" then add_obj path else
-   if F.check_suffix path ".var.ng" then add_obj path else 
-   if F.check_suffix path ".ng" then add_src devel path else
+   if is_obj path then add_obj path else
+   if F.check_suffix path ".ng" then
+      if src_exists (F.chop_extension devel ^ ".ma")
+      then add_src devel path else add_remove base path
+   else
    if src_exists devel || src_exists (devel ^ ".ma") then   
       let files = Y.readdir (F.concat base path) in
       let map base file = scan_entry base (F.concat devel file) (F.concat path file) in