X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=d0ecf9ba22d241851933a343fd6406a82cc390cb;hb=46f19eadce5f3a11c0ae26934fd8d1b597906416;hp=4f80006c6d80ebda60a6223b863c9d24a338baa7;hpb=1d15266bc05ac3524d721b66933db9a49e4c24aa;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 4f80006c6..d0ecf9ba2 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -291,11 +291,13 @@ let update_remote logger  () =
   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 *)
 
@@ -335,7 +337,7 @@ let update ?(logger = fun _ -> ()) () =
   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
@@ -462,6 +464,7 @@ let basepart_RE =
     
 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
@@ -473,6 +476,15 @@ let ls regexp =
       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")
@@ -604,7 +616,7 @@ let ls regexp =
             (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
@@ -644,5 +656,6 @@ let init () =
     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 ()