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 let chop_extension file =
26 try F.chop_extension file
27 with Invalid_argument("Filename.chop_extension") -> file
29 let src_exists path = !O.no_devel || Y.file_exists path
31 let is_obj base path =
32 if H.is_regular (F.concat base path) then
33 F.check_suffix path ".con.ng" ||
34 F.check_suffix path ".ind.ng" ||
35 F.check_suffix path ".var.ng"
38 let is_src base path =
39 H.is_regular (F.concat base path) &&
40 F.check_suffix path ".ng"
42 let is_dir base path =
43 H.is_dir (F.concat base path)
46 src_exists (chop_extension devel ^ ".ma")
49 if F.check_suffix path "/" then S.sub path 0 (pred (S.length path))
53 let path = F.chop_extension path in
54 let str = F.concat "cic:" path in
55 O.objs := US.add (U.uri_of_string str) !O.objs
57 let add_src devel path =
58 let path = F.chop_extension path in
59 let str = F.concat "cic:" path ^ "/" in
60 O.srcs := US.add (U.uri_of_string str) !O.srcs
62 let add_remove base path =
63 O.remove := F.concat base path :: !O.remove
65 let rec scan_entry inner base devel path =
66 (* Printf.eprintf "%b %s %s%!\n" inner devel path; *)
67 if is_obj base path && inner then add_obj path else
68 if is_src base path && is_script devel then add_src devel path else
69 if is_dir base path && is_script devel then scan_dir true base devel path else
70 if is_dir base path && src_exists devel then scan_dir false base devel path else
73 and scan_dir inner base devel path =
74 let files = Y.readdir (F.concat base path) in
75 let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in
76 A.iter (map base) files
78 let from_uri base devel uri =
79 O.no_devel := devel = "";
80 let str = U.string_of_uri uri in
81 let i = S.index str '/' in
82 let protocol = S.sub str 0 i in
83 if protocol = "cic:" then
84 let path = S.sub str (succ i) (S.length str - succ i) in
85 let file = mk_file path in
86 if Y.file_exists (F.concat base file) then
87 scan_entry (is_script devel) base devel file
89 else E.unsupported protocol
91 let from_string base devel s =
92 from_uri base devel (U.uri_of_string s)