X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=35a19db82bb4f5fc06afe990421085d09e147e81;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=d9e95a1c280aa098a4e900c923f7953e05606ae2;hpb=bbff1250ea4a6c74151ef00340983f2547b2e912;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index d9e95a1c2..35a19db82 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -221,14 +221,16 @@ 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_yacc.from_string doc))
+   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 ("unresolvable",[],_,_) ->
           res := Exception (Unresolvable_URI uri)
-      | Pxp_yacc.E_start_tag _ -> res := Exception UnexpectedGetterOutput
+      | Pxp_types.E_start_tag ("not_found",[],_,_) ->
+          res := Exception (Key_not_found uri)
+      | Pxp_types.E_start_tag _ -> res := Exception UnexpectedGetterOutput
       | _ -> ());
    match !res with
    | Unknown -> raise UnexpectedGetterOutput
@@ -238,8 +240,8 @@ let resolve_remote uri =
 let register_remote ~uri ~url =
   ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url)
 
-let register_remote ~uri ~url =
-  ClientHTTP.send (sprintf "%sregister?uri=%s&url=%s" (getter_url ()) uri url)
+let unregister_remote uri =
+  ClientHTTP.send (sprintf "%sunregister?uri=%s" (getter_url ()) uri)
 
 let update_remote logger  () =
   let answer = ClientHTTP.get (getter_url () ^ "update") in
@@ -261,17 +263,20 @@ let resolve uri =
   if remote () then
     resolve_remote uri
   else
-    try
-      (map_of_uri uri)#resolve uri
-    with Http_getter_map.Key_not_found _ -> raise (Unresolvable_URI uri)
+    (map_of_uri uri)#resolve uri
 
-  (* Warning: this fail if uri is already registered *)
 let register ~uri ~url =
   if remote () then
     register_remote ~uri ~url
   else
     (map_of_uri uri)#add uri url
 
+let unregister uri =
+  if remote () then
+    unregister_remote uri
+  else
+    (map_of_uri uri)#remove uri
+
 let update ?(logger = fun _ -> ()) () =
   if remote () then
     update_remote logger ()
@@ -394,24 +399,24 @@ 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) =
+       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 "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$",
+     Pcre.regexp "/$", Pcre.regexp "\\.theory$")
   in
   let (slash_RE, til_slash_RE, no_slashes_RE) =
     (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
   in
-  fun lsuri ->
+  fun regexp ->
     if remote () then
-      ls_remote lsuri
+      ls_remote regexp
     else begin
-      let pat =
-        "^" ^
-        (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
@@ -439,19 +444,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