- 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 a2ce7d9087b3fc472cf1566d655b4e5475ac7086..9f6248c0fcf39c4f540d291627eb3044624607d1 100644 (file)
--- a/matita/components/binaries/probe/matitaList.ml
+++ b/matita/components/binaries/probe/matitaList.ml
@@ -15,15 +15,18 @@ module P = Printf
 module S = String
 module Y = Sys
 
-module U = NUri
+module U  = NUri
+module US = U.UriSet
 
 module O = Options
+module E = Engine
 
-let unsupported protocol =
-   failwith (P.sprintf "probe: unsupported protocol: %s" protocol)
-
-let missing path =
-   failwith (P.sprintf "probe: missing path: %s" 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))
@@ -32,32 +35,39 @@ let mk_file path =
 let add_obj path =
    let path = F.chop_extension path in   
    let str = F.concat "cic:" path in
-   O.objs := U.uri_of_string str :: !O.objs
+   O.objs := US.add (U.uri_of_string str) !O.objs
 
-let add_src path =
-   let path = F.chop_extension path in   
-   let str = F.concat "cic:" path ^ "/" in
-   O.srcs := U.uri_of_string str :: !O.srcs
-
-let rec scan_entry base 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 path else
-   let files = Y.readdir (F.concat base path) in
-   let map base file = scan_entry base (F.concat path file) in
-   A.iter (map base) files
-
-let from_uri base uri =
+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 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 from_uri base devel uri =
+   O.no_devel := devel = "";
    let str = U.string_of_uri uri in
    let i = S.index str '/' in
    let protocol = S.sub str 0 i in
    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 file
-      else missing path
-   else unsupported protocol
+      if Y.file_exists (F.concat base file) then scan_entry base devel file
+      else E.missing path
+   else E.unsupported protocol
 
-let from_string base s =
-   from_uri base (U.uri_of_string s)
+let from_string base devel s =
+   from_uri base devel (U.uri_of_string s)