| Exception e -> raise e
| Resolved url -> url
-let deref_index_theory uri =
- if Http_getter_storage.exists (uri ^ xml_suffix) then uri
- else if is_theory_uri uri && Filename.basename uri = "index.theory" then
+let deref_index_theory ~local uri =
+(* if Http_getter_storage.exists ~local (uri ^ xml_suffix) then uri *)
+ if is_theory_uri uri && Filename.basename uri = "index.theory" then
strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
else
uri
let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
-let exists uri =
+let exists ~local uri =
(* prerr_endline ("Http_getter.exists " ^ uri); *)
if remote () then
exists_remote uri
else
- let uri = deref_index_theory uri in
- Http_getter_storage.exists (uri ^ xml_suffix)
+ let uri = deref_index_theory ~local uri in
+ Http_getter_storage.exists ~local (uri ^ xml_suffix)
let is_an_obj s =
try
s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
with UriManager.IllFormedUri _ -> true
-let resolve ~writable uri =
+let resolve ~local ~writable uri =
if remote () then
resolve_remote ~writable uri
else
- let uri = deref_index_theory uri in
+ let uri = deref_index_theory ~local uri in
try
if is_an_obj uri then
- Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+ Http_getter_storage.resolve ~writable ~local (uri ^ xml_suffix)
else
- Http_getter_storage.resolve ~writable uri
+ Http_getter_storage.resolve ~writable ~local uri
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
-let filename ~writable uri =
+let filename ~local ~writable uri =
if remote () then
raise (Key_not_found uri)
else
- let uri = deref_index_theory uri in
+ let uri = deref_index_theory ~local uri in
try
Http_getter_storage.resolve
- ~must_exists:false ~writable uri
+ ~must_exists:false ~writable ~local uri
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
let getxml uri =
if remote () then getxml_remote uri
else begin
- let uri' = deref_index_theory uri in
+ let uri' = deref_index_theory ~local:false uri in
(try
- Http_getter_storage.filename (uri' ^ xml_suffix)
+ Http_getter_storage.filename ~local:false (uri' ^ xml_suffix)
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
end
let getxslt uri =
if remote () then getxslt_remote uri
- else Http_getter_storage.filename ~find:true ("xslt:/" ^ uri)
+ else Http_getter_storage.filename ~local:false ~find:true ("xslt:/" ^ uri)
let getdtd uri =
if remote () then
let contains_object = (<>) []
(** non regexp-aware version of ls *)
-let rec dumb_ls uri_prefix =
+let rec dumb_ls ~local 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
try
store_obj objs (strip_suffix ~suffix:xml_suffix fname)
with Invalid_argument _ -> ())
- (Http_getter_storage.ls uri_prefix);
+ (Http_getter_storage.ls ~local uri_prefix);
collect_ls_items !dirs objs
end else if is_theory_uri uri_prefix then begin
let items = ref [] in
let fname = strip_suffix ~suffix:xml_suffix fname in
let theory_name = strip_suffix ~suffix:theory_suffix fname in
let sub_theory = normalize_dir cic_uri_prefix ^ theory_name ^ "/" in
- if is_empty_theory sub_theory then add_theory fname
+ if is_empty_theory ~local sub_theory then add_theory fname
with Invalid_argument _ -> ())
- (Http_getter_storage.ls uri_prefix);
+ (Http_getter_storage.ls ~local uri_prefix);
(try
- if contains_object (dumb_ls cic_uri_prefix)
- && exists (strip_trailing_slash uri_prefix ^ theory_suffix)
+ if contains_object (dumb_ls ~local cic_uri_prefix)
+ && exists ~local:false (strip_trailing_slash uri_prefix ^ theory_suffix)
then
add_theory "index.theory";
with Unresolvable_URI _ -> ());
end else
raise (Invalid_URI uri_prefix)
-and is_empty_theory uri_prefix =
+and is_empty_theory ~local uri_prefix =
(* prerr_endline ("is_empty_theory " ^ uri_prefix); *)
- not (contains_object (dumb_ls uri_prefix))
+ not (contains_object (dumb_ls ~local uri_prefix))
(* handle simple regular expressions of the form "...(..|..|..)..." on cic
* uris, not meant to be a real implementation of regexp. The only we use is
in
aux [] [] (List.concat results)
-let ls regexp =
+let ls ~local regexp =
if remote () then
ls_remote regexp
else
let prefixes = explode_ls_regexp regexp in
- merge_results (List.map dumb_ls prefixes)
+ merge_results (List.map (dumb_ls ~local) prefixes)
let getalluris () =
let rec aux acc = function
| Ls_object obj -> (dir ^ obj.uri) :: acc, subdirs
| Ls_section sect -> acc, (dir ^ sect ^ "/") :: subdirs)
(acc, todo)
- (dumb_ls dir)
+ (dumb_ls ~local:false dir)
in
aux acc' todo'
in
(* Shorthands from now on *)
let getxml' uri = getxml (UriManager.string_of_uri uri)
-let resolve' ~writable uri = resolve ~writable (UriManager.string_of_uri uri)
-let exists' uri = exists (UriManager.string_of_uri uri)
-let filename' ~writable uri = filename ~writable (UriManager.string_of_uri uri)
+let resolve' ~local ~writable uri =
+ resolve ~local ~writable (UriManager.string_of_uri uri)
+;;
+let exists' ~local uri = exists ~local (UriManager.string_of_uri uri)
+let filename' ~local ~writable uri =
+ filename ~local ~writable (UriManager.string_of_uri uri)
+;;
let tilde_expand_key k =
try