res := Exception (Unresolvable_URI uri)
| Pxp_types.E_start_tag ("not_found",[],_,_) ->
res := Exception (Key_not_found uri)
- | Pxp_types.E_start_tag _ -> res := Exception UnexpectedGetterOutput
+ | Pxp_types.E_start_tag (x,_,_,_) ->
+ res := Exception UnexpectedGetterOutput
| _ -> ());
match !res with
| Unknown -> raise UnexpectedGetterOutput
resolve_remote uri
else
(map_of_uri uri)#resolve uri
-
+
let register ~uri ~url =
if remote () then
register_remote ~uri ~url
if remote () then
unregister_remote uri
else
- (map_of_uri uri)#remove uri
+ try
+ (map_of_uri uri)#remove uri
+ with Key_not_found _ -> ()
let update ?(logger = fun _ -> ()) () =
if remote () then
if remote () then
getxml_remote ~format ~patch_dtd uri
else begin
+ Http_getter_logger.log ~level:2 ("getxml: " ^ uri);
let url = resolve uri in
+ Http_getter_logger.log ~level:2 ("resolved_uri: " ^ url) ;
let (fname, outchan) = temp_file_of_uri uri in
Http_getter_cache.respond_xml ~via_http:false ~enc:format ~patch:patch_dtd
~uri ~url outchan;
if remote () then
getxslt_remote ~patch_dtd uri
else begin
+
let url = resolve uri in
let (fname, outchan) = temp_file_of_uri uri in
Http_getter_cache.respond_xsl ~via_http:false ~url ~patch:patch_dtd outchan;
getalluris_remote ()
else
let filter uri =
- (Pcre.pmatch ~rex:heading_cic_RE uri) &&
- not (Pcre.pmatch ~rex:trailing_types_RE uri)
+ (Pcre.pmatch ~rex:heading_cic_RE uri)
+(* && not (Pcre.pmatch ~rex:trailing_types_RE uri) *)
in
return_uris (Lazy.force cic_map) filter
let dir =
"theory" ^ String.sub !dir_found 3
(String.length !dir_found - 3) ^ ".theory" in
-(*
-prerr_endline ("### " ^ uri ^ " ==> " ^ !dir_found ^ " ==> " ^ dir);
-*)
if not (List.mem dir !valid_candidates) then
valid_candidates := dir::!valid_candidates
end
then
(index_not_generated_yet := false ;
store_obj "index.theory"));
-(*
-prerr_endline ("@@@ " ^ String.concat " " !valid_candidates);
-prerr_endline ("!!! " ^ String.concat " " (List.map fst !candidates_found));
-*)
List.iter
(fun (uri,localpart) ->
if not (List.mem uri !valid_candidates) then
let getxml' uri = getxml (UriManager.string_of_uri uri)
let resolve' uri = resolve (UriManager.string_of_uri uri)
let register' uri url = register ~uri:(UriManager.string_of_uri uri) ~url
+let init () =
+ Http_getter_logger.set_log_level
+ (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level");
+ Http_getter_logger.set_log_file
+ (Helm_registry.get_opt Helm_registry.get_string "getter.log_file");
+ Http_getter_env.reload ()