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

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 2883c383c..35a19db82 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -30,7 +30,6 @@ open Printf
 
 open Http_getter_common
 open Http_getter_misc
-open Http_getter_debugger
 open Http_getter_types
 
 exception Not_implemented of string
@@ -43,6 +42,10 @@ type resolve_result =
   | Exception of exn
   | Resolved of string
 
+type logger_callback = HelmLogger.html_tag -> unit
+
+let stdout_logger tag =  print_string (HelmLogger.string_of_html_tag tag)
+
 let not_implemented s = raise (Not_implemented ("Http_getter." ^ s))
 
 let (index_line_sep_RE, index_sep_RE, trailing_types_RE,
@@ -76,8 +79,8 @@ let map_of_uri = function
   | uri when is_xsl_uri uri -> Lazy.force xsl_map
   | uri -> raise (Unresolvable_URI uri)
 
-let update_from_server logmsg server_url = (* use global maps *)
-  debug_print ("Updating information from " ^ server_url);
+let update_from_server logger server_url = (* use global maps *)
+  Http_getter_logger.log ("Updating information from " ^ server_url);
   let xml_url_of_uri = function
       (* TODO missing sanity checks on server_url, e.g. it can contains $1 *)
     | uri when (Pcre.pmatch ~rex:heading_cic_RE uri) ->
@@ -95,7 +98,8 @@ let update_from_server logmsg server_url = (* use global maps *)
         Pcre.replace ~rex:heading_rdf_theory_RE ~templ:server_url uri
     | uri -> raise (Invalid_URI uri)
   in
-  let log = ref (`T ("Processing server: " ^ server_url) :: logmsg) in
+  logger (`T ("Processing server: " ^ server_url));
+  logger `BR;
   let (xml_index, rdf_index, xsl_index) =
     (* TODO keeps index in memory, is better to keep them on temp files? *)
     (http_get (server_url ^ "/" ^ (Lazy.force Http_getter_env.xml_index)),
@@ -103,10 +107,11 @@ let update_from_server logmsg server_url = (* use global maps *)
      http_get (server_url ^ "/" ^ (Lazy.force Http_getter_env.xsl_index)))
   in
   if (xml_index = None && rdf_index = None && xsl_index = None) then
-    debug_print (sprintf "Warning: useless server %s" server_url);
+    Http_getter_logger.log (sprintf "Warning: useless server %s" server_url);
   (match xml_index with
   | Some xml_index ->
-      (log := `T "Updating XML db ...<br />" :: !log;
+      logger (`T "- Updating XML db ...");
+(*       logger `BR; *)
       List.iter
         (function
           | l when is_blank_line l -> ()  (* skip blank and commented lines *)
@@ -121,15 +126,20 @@ let update_from_server logmsg server_url = (* use global maps *)
                    assert (is_cic_uri uri || is_nuprl_uri uri) ;
                    (map_of_uri uri)#replace
                     uri ((xml_url_of_uri uri) ^ ".xml")
-                | _ -> log := `T ("Ignoring invalid line: '" ^ l) :: !log)
+                | _ ->
+                    logger (`T ("Ignoring invalid line: '" ^ l));
+                    logger `BR)
               with Invalid_URI uri ->
-                log := `T ("Ignoring invalid XML URI: '" ^ l) :: !log))
+                logger (`T ("Ignoring invalid XML URI: '" ^ l));
+                logger `BR))
         (Pcre.split ~rex:index_sep_RE xml_index); (* xml_index lines *)
-      log := `T "All done" :: !log)
+      logger (`T "All done");
+      logger `BR
   | None -> ());
   (match rdf_index with
   | Some rdf_index ->
-      (log := `T "Updating RDF db ..." :: !log;
+      logger (`T "- Updating RDF db ...");
+(*       logger `BR; *)
       List.iter
         (fun l ->
           try
@@ -140,38 +150,38 @@ let update_from_server logmsg server_url = (* use global maps *)
             | [uri] ->
                 (Lazy.force rdf_map) # replace uri
                   ((rdf_url_of_uri uri) ^ ".xml")
-            | _ -> log := `T ("Ignoring invalid line: '" ^ l) :: !log)
+            | _ ->
+                logger (`T ("Ignoring invalid line: '" ^ l));
+                logger `BR)
           with Invalid_URI uri ->
-            log := `T ("Ignoring invalid RDF URI: '" ^ l) :: !log)
+            logger (`T ("Ignoring invalid RDF URI: '" ^ l));
+            logger `BR)
         (Pcre.split ~rex:index_sep_RE rdf_index); (* rdf_index lines *)
-      log := `T "All done" :: !log)
+      logger (`T "All done");
+      logger `BR
   | None -> ());
   (match xsl_index with
   | Some xsl_index ->
-      (log := `T "Updating XSLT db ..." :: !log;
+      logger (`T "- Updating XSLT db ...");
+(*       logger `BR; *)
       List.iter
         (fun l -> (Lazy.force xsl_map) # replace l (server_url ^ "/" ^ l))
         (Pcre.split ~rex:index_sep_RE xsl_index);
-      log := `T "All done" :: !log)
+      logger (`T "All done");
+      logger `BR
   | None -> ());
-  debug_print "done with this server";
-  !log
+  Http_getter_logger.log "done with this server"
 
-let update_from_all_servers () =  (* use global maps *)
+let update_from_all_servers logger () =  (* use global maps *)
   clear_maps ();
-  let log =
-    List.fold_left
-      update_from_server
-      []  (* initial logmsg: empty *)
-        (* reverse order: 1st server is the most important one *)
-      (List.map snd (List.rev (Lazy.force Http_getter_env.servers)))
-  in
-  sync_maps ();
-  `Msg (`L (List.rev log))
+  List.iter
+    (update_from_server logger)
+      (* reverse order: 1st server is the most important one *)
+    (List.map snd (List.rev (Http_getter_env.servers ())));
+  sync_maps ()
 
-let update_from_one_server server_url =
-  let log = update_from_server [] server_url in
-  `Msg (`L (List.rev log))
+let update_from_one_server ?(logger = fun _ -> ()) server_url =
+  update_from_server logger server_url
 
 let temp_file_of_uri uri =
   let flat_string s s' c =
@@ -198,8 +208,10 @@ let getxslt_remote ~patch_dtd uri = not_implemented "getxslt_remote"
 let getdtd_remote ~patch_dtd uri = not_implemented "getdtd_remote"
 let clean_cache_remote () = not_implemented "clean_cache_remote"
 let list_servers_remote () = not_implemented "list_servers_remote"
-let add_server_remote ~position name = not_implemented "add_server_remote"
-let remove_server_remote position = not_implemented "remove_server_remote"
+let add_server_remote ~logger ~position name =
+  not_implemented "add_server_remote"
+let remove_server_remote ~logger position =
+  not_implemented "remove_server_remote"
 let getalluris_remote () = not_implemented "getalluris_remote"
 let getallrdfuris_remote () = not_implemented "getallrdfuris_remote"
 let ls_remote lsuri = not_implemented "ls_remote"
@@ -209,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 Pxp_yacc.default_config (`Entry_content [])
-    (Pxp_yacc.create_entity_manager ~is_document:true Pxp_yacc.default_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
@@ -226,19 +240,20 @@ 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 () =
+let update_remote logger  () =
   let answer = ClientHTTP.get (getter_url () ^ "update") in
-  `Msg (`T answer)
+  logger (`T answer);
+  logger `BR
 
 let getxml_remote ~format ~patch_dtd uri =
- ClientHTTP.get_and_save_to_tmp
-  (sprintf "%sgetxml?uri=%s&format=%s&patch_dtd=%s"
-    (getter_url ()) uri
-    (match format with Enc_normal -> "normal" | Enc_gzipped -> "gzipped")
-    (match patch_dtd with true -> "yes" | false -> "no"))
+  ClientHTTP.get_and_save_to_tmp
+    (sprintf "%sgetxml?uri=%s&format=%s&patch_dtd=%s"
+      (getter_url ()) uri
+      (match format with `Normal -> "normal" | `Gzipped -> "gzipped")
+      (match patch_dtd with true -> "yes" | false -> "no"))
 
 (* API *)
 
@@ -248,31 +263,34 @@ 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 update () =
+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 ()
+    update_remote logger ()
   else
-    update_from_all_servers ()
+    update_from_all_servers logger ()
 
-let getxml ?(format = Enc_normal) ?(patch_dtd = true) uri =
+let getxml ?(format = `Normal) ?(patch_dtd = true) uri =
   if remote () then
     getxml_remote ~format ~patch_dtd uri
   else begin
     let url = resolve uri in
     let (fname, outchan) = temp_file_of_uri uri in
-    Http_getter_cache.respond_xml ~uri ~url ~enc:format ~patch:patch_dtd
-      outchan;
+    Http_getter_cache.respond_xml ~via_http:false ~enc:format ~patch:patch_dtd
+      ~uri ~url outchan;
     close_out outchan;
     fname
   end
@@ -283,7 +301,7 @@ let getxslt ?(patch_dtd = true) uri =
   else begin
     let url = resolve uri in
     let (fname, outchan) = temp_file_of_uri uri in
-    Http_getter_cache.respond_xsl ~url ~patch:patch_dtd outchan;
+    Http_getter_cache.respond_xsl ~via_http:false ~url ~patch:patch_dtd outchan;
     close_out outchan;
     fname
   end
@@ -294,7 +312,7 @@ let getdtd ?(patch_dtd = true) uri =
   else begin
     let url = Lazy.force Http_getter_env.dtd_dir ^ "/" ^ uri in
     let (fname, outchan) = temp_file_of_uri uri in
-    Http_getter_cache.respond_dtd ~url ~patch:patch_dtd outchan;
+    Http_getter_cache.respond_dtd ~via_http:false ~url ~patch:patch_dtd outchan;
     close_out outchan;
     fname
   end
@@ -309,34 +327,36 @@ let list_servers () =
   if remote () then
     list_servers_remote ()
   else
-    Lazy.force Http_getter_env.servers
+    Http_getter_env.servers ()
 
-let add_server ?(position = 0) name =
+let add_server ?(logger = fun _ -> ()) ?(position = 0) name =
   if remote () then
-    add_server_remote ~position name
+    add_server_remote ~logger ~position name
   else begin
     if position = 0 then begin
       Http_getter_env.add_server ~position:0 name;
-      update_from_one_server name (* quick update (new server only) *)
+      update_from_one_server ~logger name (* quick update (new server only) *)
     end else if position > 0 then begin
       Http_getter_env.add_server ~position name;
-      update ()
-    end else  (* already checked bt parse_position *)
+      update ~logger ()
+    end else  (* already checked by parse_position *)
       assert false
   end
 
-let remove_server position =
+let has_server position = List.mem_assoc position (Http_getter_env.servers ())
+
+let remove_server ?(logger = fun _ -> ()) position =
   if remote () then
-    remove_server_remote ()
+    remove_server_remote ~logger ()
   else begin
     let server_name =
       try
-        List.assoc position (Lazy.force Http_getter_env.servers)
+        List.assoc position (Http_getter_env.servers ())
       with Not_found ->
         raise (Invalid_argument (sprintf "no server with position %d" position))
     in
     Http_getter_env.remove_server position;
-    update ()
+    update ~logger ()
   end
 
 let return_uris map filter =
@@ -379,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
@@ -424,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
@@ -444,7 +516,7 @@ let ls =
           ls_items :=
             Ls_object {
               uri = uri; ann = annflag;
-              types = typesflag; body = typesflag; proof_tree = treeflag
+              types = typesflag; body = bodyflag; proof_tree = treeflag
             } :: !ls_items)
         objs;
       List.rev !ls_items