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 rec scan_entry base devel path =
42 if F.check_suffix path ".con.ng" then add_obj path else
43 if F.check_suffix path ".ind.ng" then add_obj path else
44 if F.check_suffix path ".var.ng" then add_obj path else
45 if F.check_suffix path ".ng" then add_src devel path else
46 if src_exists devel || src_exists (devel ^ ".ma") then
47 let files = Y.readdir (F.concat base path) in
48 let map base file = scan_entry base (F.concat devel file) (F.concat path file) in
49 A.iter (map base) files
51 let from_uri base devel uri =
52 O.no_devel := devel = "";
53 let str = U.string_of_uri uri in
54 let i = S.index str '/' in
55 let protocol = S.sub str 0 i in
56 if protocol = "cic:" then
57 let path = S.sub str (succ i) (S.length str - succ i) in
58 let file = mk_file path in
59 if Y.file_exists (F.concat base file) then scan_entry base devel file
61 else E.unsupported protocol
63 let from_string base devel s =
64 from_uri base devel (U.uri_of_string s)