X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=a9884596ba62fe71ab7acfaf8f6981a49bf73c0e;hb=ebc089606ccbb3e9dbde142542a1f98f5020b4dd;hp=6192cacdccea8f264e0fa48bc1d26b649d3019cf;hpb=b866f5326c88e5881b5b7ce5354ff35abbd79549;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 6192cacdc..a9884596b 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -221,14 +221,14 @@ let resolve_remote uri =
   (* deliver resolve request to http_getter *)
   let doc = ClientHTTP.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) in
   let res = ref Unknown in
-   Pxp_yacc.process_entity PxpHelmConf.pxp_config (`Entry_content [])
-    (Pxp_yacc.create_entity_manager ~is_document:true PxpHelmConf.pxp_config
+   Pxp_ev_parser.process_entity PxpHelmConf.pxp_config (`Entry_content [])
+    (Pxp_ev_parser.create_entity_manager ~is_document:true PxpHelmConf.pxp_config
      (Pxp_yacc.from_string doc))
     (function
-      | Pxp_yacc.E_start_tag ("url",["value",url],_) -> res := Resolved url
-      | Pxp_yacc.E_start_tag ("unresolved",[],_) ->
+      | Pxp_types.E_start_tag ("url",["value",url],_,_) -> res := Resolved url
+      | Pxp_types.E_start_tag ("unresolved",[],_,_) ->
           res := Exception (Unresolvable_URI uri)
-      | Pxp_yacc.E_start_tag _ -> res := Exception UnexpectedGetterOutput
+      | Pxp_types.E_start_tag _ -> res := Exception UnexpectedGetterOutput
       | _ -> ());
    match !res with
    | Unknown -> raise UnexpectedGetterOutput
@@ -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