2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
24 let src_exists path = !O.no_devel || Y.file_exists path
27 if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
31 let path = F.chop_extension path in
32 let str = F.concat "cic:" path in
33 O.objs := US.add (U.uri_of_string str) !O.objs
35 let add_src devel path =
36 if src_exists (F.chop_extension devel ^ ".ma") then
37 let path = F.chop_extension path in
38 let str = F.concat "cic:" path ^ "/" in
39 O.srcs := US.add (U.uri_of_string str) !O.srcs
41 let add_remove base path =
42 O.remove := F.concat base path :: !O.remove
44 let rec scan_entry base devel path =
45 if F.check_suffix path ".con.ng" then add_obj path else
46 if F.check_suffix path ".ind.ng" then add_obj path else
47 if F.check_suffix path ".var.ng" then add_obj path else
48 if F.check_suffix path ".ng" then
49 if src_exists (F.chop_extension devel ^ ".ma")
50 then add_src devel path else add_remove base path
52 if src_exists devel || src_exists (devel ^ ".ma") then
53 let files = Y.readdir (F.concat base path) in
54 let map base file = scan_entry base (F.concat devel file) (F.concat path file) in
55 A.iter (map base) files
57 let from_uri base devel uri =
58 O.no_devel := devel = "";
59 let str = U.string_of_uri uri in
60 let i = S.index str '/' in
61 let protocol = S.sub str 0 i in
62 if protocol = "cic:" then
63 let path = S.sub str (succ i) (S.length str - succ i) in
64 let file = mk_file path in
65 if Y.file_exists (F.concat base file) then scan_entry base devel file
67 else E.unsupported protocol
69 let from_string base devel s =
70 from_uri base devel (U.uri_of_string s)