Back compatibility code introduced:

 1. the ls method maps a theory theory:/path/filename.theory
    to theory:/path/filename/index.theory iff there exists at least
    one object of the form cic:/path/filename/*
 2. the getter handles every URI theory:/path/filename/index.theory as
    the normalized URI theory:/path/filename.theory

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 6192cacdccea8f264e0fa48bc1d26b649d3019cf..d8d3166dceb7986101afc70d3d645ee3f41c81f3 100644 (file)
--- 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 "^[^/]*$")
@@ -409,8 +409,9 @@ let ls =
     else begin
       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, obj_RE) =
-        (Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "(\\.|$)"))
+      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
@@ -438,6 +439,18 @@ 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 _ ->
@@ -446,13 +459,51 @@ let ls =
               (* 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
+               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

diff --git a/helm/ocaml/getter/http_getter_map.ml b/helm/ocaml/getter/http_getter_map.ml
index 57ec9273639c543efafde83cac2ceeb43851f5c1..1b5d209d330a2ea8593830ffe530e6ce5d65314f 100644 (file)
--- a/helm/ocaml/getter/http_getter_map.ml
+++ b/helm/ocaml/getter/http_getter_map.ml
@@ -38,31 +38,43 @@ class map dbname =
     inherit ThreadSafe.threadSafe
 
     val mutable db = open_dbm ()
+    val index_RE = Pcre.regexp "^theory:/.*/index.theory$"
 
     (*initializer Gc.finalise Dbm.close db  (* close db on GC *)*)
 
+    (* Backward compatibility code to map
+       theory:/path/t.theory into theory:/path/t/index.theory
+       when cic:/path/t/ exists *)
+    method private normalize_key key =
+     if Pcre.pmatch ~rex:index_RE key then
+      (* we substitute /index.theory with .theory *)
+      String.sub key 0 (String.length key - 13) ^ ".theory"
+     else key
+
     method add key value =
       self#doWriter (lazy (
         try
-          Dbm.add db key value
+          Dbm.add db (self#normalize_key key) value
         with Dbm.Dbm_error "Entry already exists" -> raise (Key_already_in key)
       ))
 
     method replace key value =
       self#doWriter (lazy (
-        Dbm.replace db key value
+        Dbm.replace db (self#normalize_key key) value
       ))
 
     method remove key =
       self#doWriter (lazy (
         try
-          Dbm.remove db key
+          Dbm.remove db (self#normalize_key key)
         with Dbm.Dbm_error "dbm_delete" -> raise (Key_not_found key)
       ))
 
     method resolve key =
       self#doReader (lazy (
-        try Dbm.find db key with Not_found -> raise (Key_not_found key)
+        try
+         Dbm.find db (self#normalize_key key)
+        with Not_found -> raise (Key_not_found key)
       ))
 
     method iter (f: string -> string -> unit) =