From 58cf4ea0d6c47a940715dba1844588897772d53a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 24 May 2005 14:15:06 +0000 Subject: [PATCH] added .theory check --- helm/ocaml/getter/http_getter.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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 -- 2.39.2