- nUri : added Sets of uris for use in "probe"

[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..7af98d59c8f92d3343d0a1146debebe3a16722e9 100644 (file)
--- a/matita/components/binaries/probe/matitaList.ml
+++ b/matita/components/binaries/probe/matitaList.ml
@@ -15,15 +15,13 @@ 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 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 +30,35 @@ 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 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 rec scan_entry base path =
+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 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
+   if F.check_suffix path ".ng" then add_src devel 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 uri =
+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)