X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=d8d3166dceb7986101afc70d3d645ee3f41c81f3;hb=4767ed3aba79ed1d06c6d4e2d195b77e5bd26db5;hp=cf2ee593c8ae605225f95af3c3c74a15f70beff0;hpb=0cecccac856404634b2712fe672a6c746ed373b9;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index cf2ee593c..d8d3166dc 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -394,11 +394,11 @@ let ls =
       "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
   in
   let (types_RE, types_ann_RE, body_RE, body_ann_RE,
-       proof_tree_RE, proof_tree_ann_RE, trailing_slash_RE) =
+       proof_tree_RE, proof_tree_ann_RE, trailing_slash_RE, theory_RE) =
     (Pcre.regexp "\\.types$", Pcre.regexp "\\.types\\.ann$",
      Pcre.regexp "\\.body$", Pcre.regexp "\\.body\\.ann$",
      Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$",
-     Pcre.regexp "/$")
+     Pcre.regexp "/$", Pcre.regexp "\\.theory$")
   in
   let (slash_RE, til_slash_RE, no_slashes_RE) =
     (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
@@ -407,12 +407,11 @@ let ls =
     if remote () then
       ls_remote regexp
     else begin
-      let pat =
-        Pcre.replace ~rex:trailing_slash_RE ("^" ^ regexp)
-(*         (match lsuri with Cic p -> ("cic:" ^ p) | Theory p -> ("theory:" ^ p)) *)
-      in
-      let (dir_RE, obj_RE) =
-        (Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "(\\.|$)"))
+      let looking_for_dir = Pcre.pmatch ~rex:trailing_slash_RE regexp in
+      let pat = Pcre.replace ~rex:trailing_slash_RE ("^" ^ regexp) in
+      let (dir_RE, dir_RE2, obj_RE, orig_theory_RE) =
+        Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "/[^/]*"),
+        Pcre.regexp (pat ^ "(\\.|$)"), Pcre.regexp (pat ^ ".theory$")
       in
       let dirs = ref StringSet.empty in
       let objs = Hashtbl.create 17 in
@@ -440,19 +439,71 @@ let ls =
         in
         Hashtbl.replace objs basepart (oldflags ++ newflags)
       in
+      (* Variables used in backward compatibility code to map
+         theory:/path/t.theory into theory:/path/t/index.theory
+         when cic:/path/t/ exists *)
+      let the_candidate_for_remapping =
+       (* CSC: Here I am making a strong assumption: the pattern
+          can be only of the form  [^:]*:/path where path is
+          NOT a regular expression *)
+       "theory:" ^ Pcre.replace ~rex:(Pcre.regexp "[^:]*:") pat
+      in
+      let index_not_generated_yet = ref true in
+      let valid_candidates = ref [] in
+      let candidates_found = ref [] in
       (Lazy.force cic_map) # iter
         (* BLEARGH Dbm module lacks support for fold-like functions *)
         (fun key _ ->
           match key with
-          | uri when Pcre.pmatch ~rex:dir_RE uri ->  (* directory hit *)
+          | uri when looking_for_dir && Pcre.pmatch ~rex:dir_RE uri ->
+              (* directory hit *)
               let localpart = Pcre.replace ~rex:dir_RE uri in
               if Pcre.pmatch ~rex:no_slashes_RE localpart then
-                store_obj localpart
+               begin
+                (* Backward compatibility code to map
+		   theory:/path/t.theory into theory:/path/t/index.theory
+		   when cic:/path/t/ exists *)
+                if Pcre.pmatch ~rex:theory_RE localpart then
+                 candidates_found := (uri,localpart) :: !candidates_found
+                else
+                 store_obj localpart
+
+               end
               else
-                store_dir localpart
-          | uri when Pcre.pmatch ~rex:obj_RE  uri ->  (* file hit *)
+               begin
+                store_dir localpart ;
+                if String.sub uri 0 3 = "cic" then
+                 let dir_found = ref "" in
+                 let _ =
+                  Pcre.substitute_first ~rex:dir_RE2
+                   ~subst:(fun s -> dir_found := s; "") uri in
+                 let dir =
+                  "theory" ^ String.sub !dir_found 3
+                   (String.length !dir_found - 3) ^ ".theory" in
+(*
+prerr_endline ("### " ^ uri ^ " ==> " ^ !dir_found ^ " ==> " ^ dir);
+*)
+                 if not (List.mem dir !valid_candidates) then
+                 valid_candidates := dir::!valid_candidates
+               end
+          | uri when (not looking_for_dir) && Pcre.pmatch ~rex:obj_RE  uri ->
+              (* file hit *)
               store_obj (Pcre.replace ~rex:til_slash_RE uri)
-          | uri -> () (* miss *));
+          | uri -> (* miss *)
+             if !index_not_generated_yet &&
+	        Pcre.pmatch ~rex:orig_theory_RE uri
+             then
+              (index_not_generated_yet := false ;
+               store_obj "index.theory"));
+(*
+prerr_endline ("@@@ " ^ String.concat " " !valid_candidates);
+prerr_endline ("!!! " ^ String.concat " " (List.map fst !candidates_found));
+*)
+      List.iter
+       (fun (uri,localpart) ->
+         if not (List.mem uri !valid_candidates) then
+          store_obj localpart
+       ) !candidates_found ;
       let ls_items = ref [] in
       StringSet.iter (fun dir -> ls_items := Ls_section dir :: !ls_items) !dirs;
       Http_getter_misc.hashtbl_sorted_iter