1 exception UnableToQualify
4 let paths = List.rev (Str.split (Str.regexp "/") path) in
5 let rec build = function
6 | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
9 let paths = List.map HExtlib.normalize_path (build paths) in
10 HExtlib.find_in paths "root"
13 let is_prefix_of d1 d2 =
14 let len1 = String.length d1 in
15 let len2 = String.length d2 in
19 let pref = String.sub d2 0 len1 in
20 pref = d1 && (len1 = len2 || d2.[len1] = '/')
23 let ensure_trailing_slash s =
24 if s = "" then "/" else
25 if s.[String.length s-1] <> '/' then s^"/" else s
28 let remove_trailing_slash s =
29 if s = "" then "" else
30 let len = String.length s in
31 if s.[len-1] = '/' then String.sub s 0 (len-1) else s
34 let find_root_for ~include_paths file =
35 let include_paths = "" :: Sys.getcwd () :: include_paths in
36 let path = HExtlib.find_in include_paths file in
37 (* HLog.debug ("file "^file^" resolved as "^path); *)
38 let rootpath, root, buri =
40 let mburi = Helm_registry.get "matita.baseuri" in
41 match Str.split (Str.regexp " ") mburi with
42 | [root; buri] when is_prefix_of root path -> ":registry:", root, buri
43 | _ -> raise (Helm_registry.Key_not_found "matita.baseuri")
44 with Helm_registry.Key_not_found "matita.baseuri" ->
45 let rootpath = find_root path in
46 let data = HExtlib.input_file rootpath in
48 let lines = Str.split (Str.regexp "\n") data in
51 match Str.split (Str.regexp "=") l with
52 | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v
53 | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
56 List.assoc "baseuri" lines
58 rootpath, Filename.dirname rootpath, buri
60 (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
61 let uri = Http_getter_misc.strip_trailing_slash buri in
62 if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
63 HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
64 ensure_trailing_slash root, remove_trailing_slash uri, path
69 Helm_registry.get "matita.filename"
70 with Helm_registry.Key_not_found "matita.filename" ->
72 match Helm_registry.get_list Helm_registry.string "matita.args" with
74 HLog.warn ("Using matita.args as filename: "^x);
75 Helm_registry.set "matita.filename" x;
77 | _ -> raise (Failure "no (or more than one) filename to compile")
78 with Helm_registry.Key_not_found "matita.filename" ->
79 raise (Failure "Unable to get current file name")
82 let baseuri_of_script ?(include_paths=[]) file =
83 let root, buri, path = find_root_for ~include_paths file in
84 let path = HExtlib.normalize_path path in
85 let root = HExtlib.normalize_path root in
86 let lpath = Str.split (Str.regexp "/") path in
87 let lroot = Str.split (Str.regexp "/") root in
88 let rec substract l1 l2 =
90 | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2
92 | _ -> raise UnableToQualify
94 let extra_buri = substract lpath lroot in
96 assert(Filename.check_suffix name ".ma");
97 try Filename.chop_extension name
98 with Invalid_argument "Filename.chop_extension" -> name
101 remove_trailing_slash (HExtlib.normalize_path
102 (buri ^ "/" ^ chop (String.concat "/" extra_buri))),
106 let find_roots_in_dir dir =
107 HExtlib.find ~test:(fun f ->
108 Filename.basename f = "root" &&
109 try (Unix.stat f).Unix.st_kind = Unix.S_REG
110 with Unix.Unix_error _ -> false)