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/
30 open Http_getter_common
32 open Http_getter_types
34 exception Not_implemented of string
35 exception UnexpectedGetterOutput
42 type logger_callback = HelmLogger.html_tag -> unit
44 let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag)
46 let not_implemented s = raise (Not_implemented ("Http_getter." ^ s))
48 let index_line_sep_RE = Pcre.regexp "[ \t]+"
49 let index_sep_RE = Pcre.regexp "\r\n|\r|\n"
50 let trailing_types_RE = Pcre.regexp "\\.types$"
51 let heading_cic_RE = Pcre.regexp "^cic:"
52 let heading_theory_RE = Pcre.regexp "^theory:"
53 let heading_nuprl_RE = Pcre.regexp "^nuprl:"
54 let types_RE = Pcre.regexp "\\.types$"
55 let types_ann_RE = Pcre.regexp "\\.types\\.ann$"
56 let body_RE = Pcre.regexp "\\.body$"
57 let body_ann_RE = Pcre.regexp "\\.body\\.ann$"
58 let proof_tree_RE = Pcre.regexp "\\.proof_tree$"
59 let proof_tree_ann_RE = Pcre.regexp "\\.proof_tree\\.ann$"
60 let theory_RE = Pcre.regexp "\\.theory$"
61 let basepart_RE = Pcre.regexp
62 "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
63 let slash_RE = Pcre.regexp "/"
64 let pipe_RE = Pcre.regexp "\\|"
65 let til_slash_RE = Pcre.regexp "^.*/"
66 let no_slashes_RE = Pcre.regexp "^[^/]*$"
67 let fix_regexp_RE = Pcre.regexp ("^" ^ (Pcre.quote "(cic|theory)"))
68 let showable_file_RE =
69 Pcre.regexp "(\\.con|\\.ind|\\.var|\\.body|\\.types|\\.proof_tree)$"
71 let xml_suffix = ".xml"
72 let theory_suffix = ".theory"
74 (* global maps, shared by all threads *)
76 let ends_with_slash s =
78 s.[String.length s - 1] = '/'
79 with Invalid_argument _ -> false
81 (* should we use a remote getter or not *)
84 Helm_registry.get "getter.mode" = "remote"
85 with Helm_registry.Key_not_found _ -> false
87 let getter_url () = Helm_registry.get "getter.url"
89 (* Remote interface: getter methods implemented using a remote getter *)
92 let getxml_remote uri = not_implemented "getxml_remote"
93 let getxslt_remote uri = not_implemented "getxslt_remote"
94 let getdtd_remote uri = not_implemented "getdtd_remote"
95 let clean_cache_remote () = not_implemented "clean_cache_remote"
96 let list_servers_remote () = not_implemented "list_servers_remote"
97 let add_server_remote ~logger ~position name =
98 not_implemented "add_server_remote"
99 let remove_server_remote ~logger position =
100 not_implemented "remove_server_remote"
101 let getalluris_remote () = not_implemented "getalluris_remote"
102 let ls_remote lsuri = not_implemented "ls_remote"
103 let exists_remote uri = not_implemented "exists_remote"
106 let resolve_remote uri =
107 (* deliver resolve request to http_getter *)
109 Http_getter_wget.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri)
111 let res = ref Unknown in
112 let start_element tag attrs =
116 res := Resolved (List.assoc "value" attrs)
117 with Not_found -> ())
118 | "unresolvable" -> res := Exception (Unresolvable_URI uri)
119 | "not_found" -> res := Exception (Key_not_found uri)
123 XmlPushParser.default_callbacks with
124 XmlPushParser.start_element = Some start_element
126 let xml_parser = XmlPushParser.create_parser callbacks in
127 XmlPushParser.parse xml_parser (`String doc);
128 XmlPushParser.final xml_parser;
130 | Unknown -> raise UnexpectedGetterOutput
131 | Exception e -> raise e
132 | Resolved url -> url
134 let deref_index_theory uri =
135 if Http_getter_storage.exists (uri ^ xml_suffix) then uri
136 else if is_theory_uri uri && Filename.basename uri = "index.theory" then
137 strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
143 let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
146 (* prerr_endline ("Http_getter.exists " ^ uri); *)
150 let uri = deref_index_theory uri in
151 Http_getter_storage.exists (uri ^ xml_suffix)
157 let uri = deref_index_theory uri in
159 Http_getter_storage.resolve (uri ^ xml_suffix)
160 with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
163 if remote () then getxml_remote uri
165 let uri' = deref_index_theory uri in
167 Http_getter_storage.filename (uri' ^ xml_suffix)
168 with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
172 if remote () then getxslt_remote uri
173 else Http_getter_storage.filename ~find:true ("xslt:/" ^ uri)
179 let fname = Lazy.force Http_getter_env.dtd_dir ^ "/" ^ uri in
180 if not (Sys.file_exists fname) then raise (Dtd_not_found uri);
186 clean_cache_remote ()
188 Http_getter_storage.clean_cache ()
190 let (++) (oldann, oldtypes, oldbody, oldtree)
191 (newann, newtypes, newbody, newtree) =
192 ((if newann > oldann then newann else oldann),
193 (if newtypes > oldtypes then newtypes else oldtypes),
194 (if newbody > oldbody then newbody else oldbody),
195 (if newtree > oldtree then newtree else oldtree))
197 let store_obj tbl o =
198 (* prerr_endline ("Http_getter.store_obj " ^ o); *)
199 if Pcre.pmatch ~rex:showable_file_RE o then begin
200 let basepart = Pcre.replace ~rex:basepart_RE ~templ:"$1" o in
201 let no_flags = false, No, No, No in
204 Hashtbl.find tbl basepart
205 with Not_found -> (* no ann, no types, no body, no proof tree *)
210 | s when Pcre.pmatch ~rex:types_RE s -> (false, Yes, No, No)
211 | s when Pcre.pmatch ~rex:types_ann_RE s -> (true, Ann, No, No)
212 | s when Pcre.pmatch ~rex:body_RE s -> (false, No, Yes, No)
213 | s when Pcre.pmatch ~rex:body_ann_RE s -> (true, No, Ann, No)
214 | s when Pcre.pmatch ~rex:proof_tree_RE s -> (false, No, No, Yes)
215 | s when Pcre.pmatch ~rex:proof_tree_ann_RE s -> (true, No, No, Ann)
218 Hashtbl.replace tbl basepart (oldflags ++ newflags)
221 let store_dir set_ref d =
222 set_ref := StringSet.add (List.hd (Pcre.split ~rex:slash_RE d)) !set_ref
224 let collect_ls_items dirs_set objs_tbl =
225 let items = ref [] in
226 StringSet.iter (fun dir -> items := Ls_section dir :: !items) dirs_set;
227 Http_getter_misc.hashtbl_sorted_iter
228 (fun uri (annflag, typesflag, bodyflag, treeflag) ->
231 uri = uri; ann = annflag;
232 types = typesflag; body = bodyflag; proof_tree = treeflag
237 let contains_object = (<>) []
239 (** non regexp-aware version of ls *)
240 let rec dumb_ls uri_prefix =
241 (* prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix); *)
242 if is_cic_obj_uri uri_prefix then begin
243 let dirs = ref StringSet.empty in
244 let objs = Hashtbl.create 17 in
247 if ends_with_slash fname then
251 store_obj objs (strip_suffix ~suffix:xml_suffix fname)
252 with Invalid_argument _ -> ())
253 (Http_getter_storage.ls uri_prefix);
254 collect_ls_items !dirs objs
255 end else if is_theory_uri uri_prefix then begin
256 let items = ref [] in
257 let add_theory fname =
260 uri = fname; ann = false; types = No; body = No; proof_tree = No }
264 Pcre.replace_first ~rex:heading_theory_RE ~templ:"cic:" uri_prefix
268 if ends_with_slash fname then
269 items := Ls_section (strip_trailing_slash fname) :: !items
272 let fname = strip_suffix ~suffix:xml_suffix fname in
273 let theory_name = strip_suffix ~suffix:theory_suffix fname in
274 let sub_theory = normalize_dir cic_uri_prefix ^ theory_name ^ "/" in
275 if is_empty_theory sub_theory then add_theory fname
276 with Invalid_argument _ -> ())
277 (Http_getter_storage.ls uri_prefix);
279 if contains_object (dumb_ls cic_uri_prefix)
280 && exists (strip_trailing_slash uri_prefix ^ theory_suffix)
282 add_theory "index.theory";
283 with Unresolvable_URI _ -> ());
286 raise (Invalid_URI uri_prefix)
288 and is_empty_theory uri_prefix =
289 (* prerr_endline ("is_empty_theory " ^ uri_prefix); *)
290 not (contains_object (dumb_ls uri_prefix))
292 (* handle simple regular expressions of the form "...(..|..|..)..." on cic
293 * uris, not meant to be a real implementation of regexp. The only we use is
294 * "(cic|theory):/..." *)
295 let explode_ls_regexp regexp =
297 let len = String.length regexp in
298 let lparen_idx = String.index regexp '(' in
299 let rparen_idx = String.index_from regexp lparen_idx ')' in
300 let choices_str = (* substring between parens, parens excluded *)
301 String.sub regexp (lparen_idx + 1) (rparen_idx - lparen_idx - 1)
303 let choices = Pcre.split ~rex:pipe_RE choices_str in
304 let prefix = String.sub regexp 0 lparen_idx in
305 let suffix = String.sub regexp (rparen_idx + 1) (len - (rparen_idx + 1)) in
306 List.map (fun choice -> prefix ^ choice ^ suffix) choices
307 with Not_found -> [regexp]
309 let merge_results results =
310 let rec aux objects_acc dirs_acc = function
311 | [] -> dirs_acc @ objects_acc
312 | Ls_object _ as obj :: tl -> aux (obj :: objects_acc) dirs_acc tl
313 | Ls_section _ as dir :: tl ->
314 if List.mem dir dirs_acc then (* filters out dir duplicates *)
315 aux objects_acc dirs_acc tl
317 aux objects_acc (dir :: dirs_acc) tl
319 aux [] [] (List.concat results)
325 let prefixes = explode_ls_regexp regexp in
326 merge_results (List.map dumb_ls prefixes)
329 let rec aux acc = function
334 (fun (acc, subdirs) result ->
336 | Ls_object obj -> (dir ^ obj.uri) :: acc, subdirs
337 | Ls_section sect -> acc, (dir ^ sect ^ "/") :: subdirs)
343 aux [] ["cic:/"] (* trailing slash required *)
345 (* Shorthands from now on *)
347 let getxml' uri = getxml (UriManager.string_of_uri uri)
348 let resolve' uri = resolve (UriManager.string_of_uri uri)
349 let exists' uri = exists (UriManager.string_of_uri uri)
351 let tilde_expand_key k =
353 Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
354 with Helm_registry.Key_not_found _ -> ()
357 List.iter tilde_expand_key ["getter.cache_dir"; "getter.dtd_dir"];
358 Http_getter_logger.set_log_level
359 (Helm_registry.get_opt_default Helm_registry.int ~default:1
361 Http_getter_logger.set_log_file
362 (Helm_registry.get_opt Helm_registry.string "getter.log_file")