exception Not_implemented of string
exception UnexpectedGetterOutput
-(* resolve_result is needed because it is not possible to raise *)
-(* an exception in a pxp ever-processing callback. Too bad. *)
type resolve_result =
| Unknown
| Exception of exn
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
- Pxp_ev_parser.process_entity PxpHelmConf.pxp_config (`Entry_content [])
- (Pxp_ev_parser.create_entity_manager ~is_document:true
- PxpHelmConf.pxp_config (Pxp_yacc.from_string doc))
- (function
- | Pxp_types.E_start_tag ("url",["value",url],_,_) -> res := Resolved url
- | Pxp_types.E_start_tag ("unresolvable",[],_,_) ->
- res := Exception (Unresolvable_URI uri)
- | Pxp_types.E_start_tag ("not_found",[],_,_) ->
- res := Exception (Key_not_found uri)
- | Pxp_types.E_start_tag (x,_,_,_) ->
- res := Exception UnexpectedGetterOutput
- | _ -> ());
- match !res with
- | Unknown -> raise UnexpectedGetterOutput
- | Exception e -> raise e
- | Resolved url -> url
+ let start_element tag attrs =
+ match tag with
+ | "url" ->
+ (try
+ res := Resolved (List.assoc "value" attrs)
+ with Not_found -> ())
+ | "unresolvable" -> res := Exception (Unresolvable_URI uri)
+ | "not_found" -> res := Exception (Key_not_found uri)
+ | _ -> ()
+ in
+ let callbacks = {
+ XmlPushParser.default_callbacks with
+ XmlPushParser.start_element = Some start_element
+ } in
+ let xml_parser = XmlPushParser.create_parser callbacks in
+ XmlPushParser.parse xml_parser (`String doc);
+ XmlPushParser.final xml_parser;
+ match !res with
+ | Unknown -> raise UnexpectedGetterOutput
+ | Exception e -> raise e
+ | 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
let getxml_remote ~format ~patch_dtd uri =
- ClientHTTP.get_and_save_to_tmp
- (sprintf "%sgetxml?uri=%s&format=%s&patch_dtd=%s"
+ let uri =
+ sprintf "%sgetxml?uri=%s&format=%s&patch_dtd=%s"
(getter_url ()) uri
- (match format with `Normal -> "normal" | `Gzipped -> "gzipped")
- (match patch_dtd with true -> "yes" | false -> "no"))
+ (match format with `Normal -> "normal" | `Gzipped -> "gz")
+ (match patch_dtd with true -> "yes" | false -> "no")
+ in
+ Http_getter_wget.get_and_save_to_tmp uri
(* API *)
else
update_from_all_servers logger ()
-let getxml ?(format = `Normal) ?(patch_dtd = true) uri =
+let getxml ?(format = `Gzipped) ?(patch_dtd = false) uri =
if remote () then
getxml_remote ~format ~patch_dtd uri
else begin
let (slash_RE, til_slash_RE, no_slashes_RE) =
(Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
+let fix_regexp_RE = Pcre.regexp ("^" ^ (Pcre.quote "(cic|theory)"))
let ls regexp =
if remote () then
Pcre.regexp (pat ^ "/"), Pcre.regexp "[^/]+/[^/]*",
Pcre.regexp (pat ^ "(\\.|$)"), Pcre.regexp "/.*"
in
+ let exists_theory regexp =
+ let theory =
+ Pcre.replace ~rex:fix_regexp_RE ~templ:"theory" regexp ^ "index.theory"
+ in
+ try
+ ignore (resolve theory);
+ true
+ with Key_not_found _ -> false
+ in
let toplevel_theory =
match List.rev (Pcre.split ~rex:slash_RE pat) with
| dir :: _ -> Some (dir ^ ".theory")
(index_not_generated_yet := false ;
store_obj "index.theory"));
*)
- store_obj "index.theory";
+ if exists_theory regexp then store_obj "index.theory";
List.iter
(fun localpart ->
if not (List.mem localpart !valid_candidates) then
let init () =
Http_getter_logger.set_log_level
- (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level");
+ (Helm_registry.get_opt_default Helm_registry.int ~default:1
+ "getter.log_level");
Http_getter_logger.set_log_file
- (Helm_registry.get_opt Helm_registry.get_string "getter.log_file");
+ (Helm_registry.get_opt Helm_registry.string "getter.log_file");
Http_getter_env.reload ();
let is_prefetch_set =
- Helm_registry.get_opt_default Helm_registry.get_bool false "getter.prefetch"
+ Helm_registry.get_opt_default Helm_registry.bool ~default:false
+ "getter.prefetch"
in
if is_prefetch_set then
- ignore (Thread.create sync_with_map ())
+ (* ignore (Thread.create sync_with_map ()) *)
+ sync_with_map ()