X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=0251c548f8aa0b409d7ebc0cfd95856c8759571a;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=e0a1a4658c500f3f74ed06820657138828cd3594;hpb=52fdcda3e0083391fa04a064f3e07279d975d5ba;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index e0a1a4658..0251c548f 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -464,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
@@ -475,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")
@@ -606,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