X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2FmatitaList.ml;h=22b2f91b58aa4d6242048e236587fe10fe59eeb1;hb=50001ac0b45a3f6376e8cbfd9200149a01d68148;hp=9f6248c0fcf39c4f540d291627eb3044624607d1;hpb=c559209567ff7ec5e4d3de7fef431398f9ba2559;p=helm.git

diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml
index 9f6248c0f..22b2f91b5 100644
--- a/matita/components/binaries/probe/matitaList.ml
+++ b/matita/components/binaries/probe/matitaList.ml
@@ -17,17 +17,34 @@ module Y = Sys
 
 module U  = NUri
 module US = U.UriSet
+module H  = HExtlib
 
 module O = Options
 module E = Engine
 
-let is_obj path = 
-   F.check_suffix path ".con.ng" ||
-   F.check_suffix path ".ind.ng" ||
-   F.check_suffix path ".var.ng"
-  
+let chop_extension file =
+   try F.chop_extension file
+   with Invalid_argument("Filename.chop_extension") -> file
+
 let src_exists path = !O.no_devel || Y.file_exists path
 
+let is_obj base path = 
+   if H.is_regular (F.concat base path) then
+      F.check_suffix path ".con.ng" ||
+      F.check_suffix path ".ind.ng" ||
+      F.check_suffix path ".var.ng"
+  else false
+
+let is_src base path = 
+   H.is_regular (F.concat base path) &&
+   F.check_suffix path ".ng"
+
+let is_dir base path =
+   H.is_dir (F.concat base path)
+
+let is_script devel =
+   src_exists (chop_extension devel ^ ".ma")
+
 let mk_file path =
    if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
    else path ^ ".ng"
@@ -38,24 +55,25 @@ let add_obj path =
    O.objs := US.add (U.uri_of_string str) !O.objs
 
 let add_src devel path =
-   if src_exists (F.chop_extension devel ^ ".ma") then
-      let path = F.chop_extension path in   
-      let str = F.concat "cic:" path ^ "/" in
-      O.srcs := US.add (U.uri_of_string str) !O.srcs
+   let path = F.chop_extension path in   
+   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 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
-      A.iter (map base) files
+let rec scan_entry inner base devel path =
+(*   Printf.eprintf "%b %s %s%!\n" inner devel path; *)
+   if is_obj base path && inner then add_obj path else
+   if is_src base path && is_script devel then add_src devel path else 
+   if is_dir base path && is_script devel then scan_dir true base devel path else
+   if is_dir base path && src_exists devel then scan_dir false base devel path else
+   add_remove base path
+
+and scan_dir inner base devel path =
+   let files = Y.readdir (F.concat base path) in
+   let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in
+   A.iter (map base) files
 
 let from_uri base devel uri =
    O.no_devel := devel = "";
@@ -65,7 +83,8 @@ let from_uri base devel uri =
    if protocol = "cic:" then 
       let path = S.sub str (succ i) (S.length str - succ i) in
       let file = mk_file path in
-      if Y.file_exists (F.concat base file) then scan_entry base devel file
+      if Y.file_exists (F.concat base file) then
+         scan_entry (is_script devel) base devel file 
       else E.missing path
    else E.unsupported protocol