let til_slash_RE = Pcre.regexp "^.*/"
let no_slashes_RE = Pcre.regexp "^[^/]*$"
let fix_regexp_RE = Pcre.regexp ("^" ^ (Pcre.quote "(cic|theory)"))
-let showable_file_RE = Pcre.regexp "(\\.con|\\.ind|\\.var)$"
+let showable_file_RE =
+ Pcre.regexp "(\\.con|\\.ind|\\.var|\\.body|\\.types|\\.proof_tree)$"
let xml_suffix = ".xml"
-let theory_suffix = ".theory" ^ xml_suffix
+let theory_suffix = ".theory"
(* global maps, shared by all threads *)
(* <TODO> *)
let getxml_remote uri = not_implemented "getxml_remote"
-let getxslt_remote ~patch_dtd uri = not_implemented "getxslt_remote"
+let getxslt_remote uri = not_implemented "getxslt_remote"
let getdtd_remote uri = not_implemented "getdtd_remote"
let clean_cache_remote () = not_implemented "clean_cache_remote"
let list_servers_remote () = not_implemented "list_servers_remote"
| 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
+ strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
+ else
+ uri
+
(* API *)
let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
let exists 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 resolve uri =
if remote () then
resolve_remote uri
else
+ let uri = deref_index_theory uri in
try
Http_getter_storage.resolve (uri ^ xml_suffix)
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
let getxml uri =
- if remote () then
- getxml_remote uri
+ if remote () then getxml_remote uri
else begin
- try
- 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
+ Http_getter_storage.filename (uri' ^ xml_suffix)
+ with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
end
-let getxslt ?(patch_dtd = true) uri = assert false
-(* let getxslt ?(patch_dtd = true) uri =
- 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;
- close_out outchan;
- fname
- end *)
+let getxslt uri =
+ if remote () then getxslt_remote uri
+ else Http_getter_storage.filename ~find:true ("xslt:/" ^ uri)
let getdtd uri =
if remote () then
(if newtree > oldtree then newtree else oldtree))
let store_obj tbl o =
+(* prerr_endline ("Http_getter.store_obj " ^ o); *)
if Pcre.pmatch ~rex:showable_file_RE o then begin
let basepart = Pcre.replace ~rex:basepart_RE ~templ:"$1" o in
let no_flags = false, No, No, No in
objs_tbl;
List.rev !items
+let contains_object = (<>) []
+
(** non regexp-aware version of ls *)
-let dumb_ls uri_prefix =
+let rec 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
collect_ls_items !dirs objs
end else if is_theory_uri uri_prefix then begin
let items = ref [] in
+ let add_theory fname =
+ items :=
+ Ls_object {
+ uri = fname; ann = false; types = No; body = No; proof_tree = No }
+ :: !items
+ in
+ let cic_uri_prefix =
+ Pcre.replace_first ~rex:heading_theory_RE ~templ:"cic:" uri_prefix
+ in
List.iter
(fun fname ->
if ends_with_slash fname then
items := Ls_section (strip_trailing_slash fname) :: !items
else
try
- let obj =
- { uri = strip_suffix theory_suffix fname;
- ann = false; types = No; body = No; proof_tree = No }
- in
- items := Ls_object obj :: !items
+ 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
with Invalid_argument _ -> ())
(Http_getter_storage.ls uri_prefix);
+ (try
+ if contains_object (dumb_ls cic_uri_prefix)
+ && exists (strip_trailing_slash uri_prefix ^ theory_suffix)
+ then
+ add_theory "index.theory";
+ with Unresolvable_URI _ -> ());
!items
end else
raise (Invalid_URI uri_prefix)
+and 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
* uris, not meant to be a real implementation of regexp. The only we use is
* "(cic|theory):/..." *)
let resolve' uri = resolve (UriManager.string_of_uri uri)
let exists' uri = exists (UriManager.string_of_uri uri)
+let tilde_expand_key k =
+ try
+ Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
+ with Helm_registry.Key_not_found _ -> ()
+
let init () =
+ List.iter tilde_expand_key ["getter.cache_dir"; "getter.dtd_dir"];
Http_getter_logger.set_log_level
(Helm_registry.get_opt_default Helm_registry.int ~default:1
"getter.log_level");
projects / helm.git / blobdiff