type logger_callback = HelmLogger.html_tag -> unit
-let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag)
+let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag)
let not_implemented s = raise (Not_implemented ("Http_getter." ^ s))
-let (index_line_sep_RE, index_sep_RE, trailing_types_RE,
- heading_cic_RE, heading_theory_RE, heading_nuprl_RE,
- heading_rdf_cic_RE, heading_rdf_theory_RE) =
- (Pcre.regexp "[ \t]+", Pcre.regexp "\r\n|\r|\n",
- Pcre.regexp "\\.types$",
- Pcre.regexp "^cic:", Pcre.regexp "^theory:", Pcre.regexp "^nuprl:",
- Pcre.regexp "^helm:rdf.*//cic:", Pcre.regexp "^helm:rdf.*//theory:")
+let index_line_sep_RE = Pcre.regexp "[ \t]+"
+let index_sep_RE = Pcre.regexp "\r\n|\r|\n"
+let trailing_types_RE = Pcre.regexp "\\.types$"
+let heading_cic_RE = Pcre.regexp "^cic:"
+let heading_theory_RE = Pcre.regexp "^theory:"
+let heading_nuprl_RE, = Pcre.regexp "^nuprl:"
+let heading_rdf_cic_RE = Pcre.regexp "^helm:rdf.*//cic:"
+let heading_rdf_theory_RE = Pcre.regexp "^helm:rdf.*//theory:"
(* global maps, shared by all threads *)
let resolve_remote uri =
(* deliver resolve request to http_getter *)
- let doc = ClientHTTP.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) in
+ let doc =
+ Http_getter_wget.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri)
+ in
let res = ref Unknown in
let start_element tag attrs =
match tag with
| Resolved url -> url
let register_remote ~uri ~url =
- ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url)
+ Http_getter_wget.send
+ (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url)
let unregister_remote uri =
- ClientHTTP.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri)
+ Http_getter_wget.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri)
let update_remote logger () =
- let answer = ClientHTTP.get (getter_url () ^ "update") in
+ let answer = Http_getter_wget.get (getter_url () ^ "update") in
logger (`T answer);
logger `BR
(match format with `Normal -> "normal" | `Gzipped -> "gz")
(match patch_dtd with true -> "yes" | false -> "no")
in
- ClientHTTP.get_and_save_to_tmp uri
+ Http_getter_wget.get_and_save_to_tmp uri
(* API *)