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_______________________________________________________________ *)
25 F.check_suffix path ".con.ng" ||
26 F.check_suffix path ".ind.ng" ||
27 F.check_suffix path ".var.ng"
29 let src_exists path = !O.no_devel || Y.file_exists path
32 if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
36 let path = F.chop_extension path in
37 let str = F.concat "cic:" path in
38 O.objs := US.add (U.uri_of_string str) !O.objs
40 let add_src devel path =
41 if src_exists (F.chop_extension devel ^ ".ma") then
42 let path = F.chop_extension path in
43 let str = F.concat "cic:" path ^ "/" in
44 O.srcs := US.add (U.uri_of_string str) !O.srcs
46 let add_remove base path =
47 O.remove := F.concat base path :: !O.remove
49 let rec scan_entry base devel path =
50 if is_obj path then add_obj path else
51 if F.check_suffix path ".ng" then
52 if src_exists (F.chop_extension devel ^ ".ma")
53 then add_src devel path else add_remove base path
55 if src_exists devel || src_exists (devel ^ ".ma") then
56 let files = Y.readdir (F.concat base path) in
57 let map base file = scan_entry base (F.concat devel file) (F.concat path file) in
58 A.iter (map base) files
60 let from_uri base devel uri =
61 O.no_devel := devel = "";
62 let str = U.string_of_uri uri in
63 let i = S.index str '/' in
64 let protocol = S.sub str 0 i in
65 if protocol = "cic:" then
66 let path = S.sub str (succ i) (S.length str - succ i) in
67 let file = mk_file path in
68 if Y.file_exists (F.concat base file) then scan_entry base devel file
70 else E.unsupported protocol
72 let from_string base devel s =
73 from_uri base devel (U.uri_of_string s)