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_______________________________________________________________ *)
21 let unsupported protocol =
22 failwith (P.sprintf "probe: unsupported protocol: %s" protocol)
25 failwith (P.sprintf "probe: missing path: %s" path)
28 failwith (P.sprintf "probe: missing root: %s" path)
30 let out_int i = P.printf "%u\n" i
32 let out_length uris = out_int (US.cardinal uris)
35 let map uri = P.printf "%s\n" (U.string_of_uri uri) in
39 F.check_suffix str ".conf.xml"
42 let str = H.normalize_path str in
44 if H.is_regular str && F.check_suffix str ".ma"
45 then F.dirname str, F.chop_extension (F.basename str)
46 else if H.is_dir str then str, ""
49 let rec aux bdir file = match B.find_roots_in_dir bdir with
51 let buri = L.assoc "baseuri" (B.load_root_file root) in
52 F.concat bdir file, F.concat buri file
54 if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir else
55 aux (F.dirname bdir) (F.concat (F.basename bdir) file)