let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
let exists uri =
- prerr_endline ("Http_getter.exists " ^ uri);
+(* prerr_endline ("Http_getter.exists " ^ uri); *)
if remote () then
exists_remote uri
else
let getxml uri =
if remote () then getxml_remote uri
else begin
- try
- let uri = deref_index_theory uri in
- Http_getter_storage.filename (uri ^ xml_suffix)
- with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
+ let uri' = deref_index_theory uri in
+ (try
+ try
+ Http_getter_storage.filename (uri' ^ xml_suffix)
+ with Http_getter_storage.Resource_not_found _ as exn ->
+ if uri <> uri' then Http_getter_storage.filename (uri ^ xml_suffix)
+ else raise exn
+ with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
end
let getxslt uri =
List.rev !items
let contains_object = (<>) []
-(* List.iter
- (function
- | Ls_section name -> prerr_endline (name ^ "/");
- | Ls_object obj -> prerr_endline obj.uri)
- l;
- prerr_endline (string_of_bool b);
- b *)
-(* List.exists (function Ls_object _ -> true | _ -> false) *)
(** non regexp-aware version of ls *)
let rec dumb_ls uri_prefix =
- prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix);
+(* prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix); *)
if is_cic_obj_uri uri_prefix then begin
let dirs = ref StringSet.empty in
let objs = Hashtbl.create 17 in
raise (Invalid_URI uri_prefix)
and is_empty_theory uri_prefix =
- prerr_endline ("is_empty_theory " ^ uri_prefix);
+(* prerr_endline ("is_empty_theory " ^ uri_prefix); *)
not (contains_object (dumb_ls uri_prefix))
(* handle simple regular expressions of the form "...(..|..|..)..." on cic