1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 exception NoRootFor of string
30 if String.length path > 0 && path.[0] <> '/' then
31 Sys.getcwd () ^ "/" ^ path
35 HExtlib.normalize_path path
40 let path = absolutize path in
41 let paths = List.rev (Str.split (Str.regexp "/") path) in
42 let rec build = function
43 | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
46 let paths = List.map HExtlib.normalize_path (build paths) in
47 try HExtlib.find_in paths "root"
48 with Failure "find_in" ->
49 raise (NoRootFor (path ^ " (" ^ String.concat ", " paths ^ ")"))
52 let ensure_trailing_slash s =
53 if s = "" then "/" else
54 if s.[String.length s-1] <> '/' then s^"/" else s
57 let remove_trailing_slash s =
58 if s = "" then "" else
59 let len = String.length s in
60 if s.[len-1] = '/' then String.sub s 0 (len-1) else s
63 let load_root_file rootpath =
64 let data = HExtlib.input_file rootpath in
65 let lines = Str.split (Str.regexp "\n") data in
67 Pcre.replace ~pat:"[ \t]+" ~templ:" "
68 (Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s))
72 match Str.split (Str.regexp "=") l with
73 | [k;v] -> clean k, Http_getter_misc.strip_trailing_slash (clean v)
74 | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
78 let find_root_for ~include_paths file =
79 let include_paths = "" :: Sys.getcwd () :: include_paths in
80 let rec find_path_for file =
81 try HExtlib.find_in include_paths file
82 with Failure "find_in" ->
83 if Filename.check_suffix file ".ma" then begin
84 let mma = Filename.chop_suffix file ".ma" ^ ".mma" in
85 HLog.warn ("We look for: " ^ mma);
86 let path = find_path_for mma in
87 Filename.chop_suffix path ".mma" ^ ".ma"
89 HLog.error ("We are in: " ^ Sys.getcwd ());
90 HLog.error ("Unable to find: "^file^"\nPaths explored:");
91 List.iter (fun x -> HLog.error (" - "^x)) include_paths;
92 raise (NoRootFor file)
95 let path = find_path_for file in
96 let path = absolutize path in
97 (* HLog.debug ("file "^file^" resolved as "^path); *)
98 let rootpath, root, buri =
100 let mburi = Helm_registry.get "matita.baseuri" in
101 match Str.split (Str.regexp " ") mburi with
102 | [root; buri] when HExtlib.is_prefix_of root path ->
103 ":registry:", root, buri
104 | _ -> raise (Helm_registry.Key_not_found "matita.baseuri")
105 with Helm_registry.Key_not_found "matita.baseuri" ->
106 let rootpath = find_root path in
107 let buri = List.assoc "baseuri" (load_root_file rootpath) in
108 rootpath, Filename.dirname rootpath, buri
110 (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
111 let uri = Http_getter_misc.strip_trailing_slash buri in
112 if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
113 HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
114 ensure_trailing_slash root, remove_trailing_slash uri, path
118 let mk_baseuri root extra =
120 assert(Filename.check_suffix name ".ma" ||
121 Filename.check_suffix name ".mma");
122 try Filename.chop_extension name
123 with Invalid_argument "Filename.chop_extension" -> name
125 remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra))
128 let baseuri_of_script ~include_paths file =
129 let root, buri, path = find_root_for ~include_paths file in
130 let path = HExtlib.normalize_path path in
131 let root = HExtlib.normalize_path root in
132 let lpath = Str.split (Str.regexp "/") path in
133 let lroot = Str.split (Str.regexp "/") root in
134 let rec substract l1 l2 =
136 | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2
138 | _ -> raise (NoRootFor (file ^" "^path^" "^root))
140 let extra_buri = substract lpath lroot in
141 let extra = String.concat "/" extra_buri in
143 mk_baseuri buri extra,
148 let find_roots_in_dir dir =
149 HExtlib.find ~test:(fun f ->
150 Filename.basename f = "root" &&
151 try (Unix.stat f).Unix.st_kind = Unix.S_REG
152 with Unix.Unix_error _ -> false)
156 (* scheme uri part as defined in URI Generic Syntax (RFC 3986) *)
157 let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:"
159 let is_uri str = Pcre.pmatch ~rex:uri_scheme_rex str