From: Claudio Sacerdoti Coen Date: Sun, 30 May 2004 22:14:49 +0000 (+0000) Subject: Back compatibility code introduced: X-Git-Tag: pre_subst_in_kernel~47 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0224ce3e20ff502b7ce04865bc23ed99a47c764d;p=helm.git 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 6192cacdc..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 "^[^/]*$") @@ -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 57ec92736..1b5d209d3 100644 --- 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) =