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
+ ClientHTTP.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
Helm_registry.get_opt_default Helm_registry.get_bool false "getter.prefetch"
in
if is_prefetch_set then
- ignore (Thread.create sync_with_map ())
+ (* ignore (Thread.create sync_with_map ()) *)
+ sync_with_map ()