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_______________________________________________________________ *)
26 let chop_extension file =
27 try F.chop_extension file
28 with Invalid_argument _ -> file
30 let script devel = chop_extension devel ^ ".ma"
32 let src_exists path = !O.no_devel || Y.file_exists path
34 let is_obj base path =
35 if H.is_regular (F.concat base path) then
36 F.check_suffix path ".con.ng" ||
37 F.check_suffix path ".ind.ng" ||
38 F.check_suffix path ".var.ng"
41 let is_src base path =
42 H.is_regular (F.concat base path) &&
43 F.check_suffix path ".ng"
45 let is_dir base path =
46 H.is_dir (F.concat base path)
49 src_exists (script devel)
52 if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
56 let path = F.chop_extension path in
57 let str = F.concat "cic:" path in
58 O.objs := US.add (U.uri_of_string str) !O.objs
60 let add_src devel path =
61 let path = F.chop_extension path in
62 let str = F.concat "cic:" path ^ "/" in
63 O.srcs := US.add (U.uri_of_string str) !O.srcs;
66 let add_remove base path =
67 O.remove := F.concat base path :: !O.remove
69 let rec scan_entry inner base devel path =
70 (* Printf.eprintf "%b %s %s%!\n" inner devel path; *)
71 if is_obj base path && inner then add_obj path else
72 if is_src base path && is_script devel then add_src devel path else
73 if is_dir base path && is_script devel then scan_dir true base devel path else
74 if is_dir base path && src_exists devel then scan_dir false base devel path else
77 and scan_dir inner base devel path =
78 let files = Y.readdir (F.concat base path) in
79 let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in
80 A.iter (map base) files
82 let from_uri base devel uri =
83 O.no_devel := devel = "";
84 let str = U.string_of_uri uri in
85 let i = S.index str '/' in
86 let protocol = S.sub str 0 i in
87 if protocol = "cic:" then
88 let path = S.sub str (succ i) (S.length str - succ i) in
89 let file = mk_file path in
90 if Y.file_exists (F.concat base file) then
91 scan_entry (is_script devel) base devel file
93 else X.unsupported protocol
95 let from_string base devel s =
96 from_uri base devel (U.uri_of_string s)