X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=f7ca2388c89b9653d04f8087ac4d021fc8d1e966;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=d8d3166dceb7986101afc70d3d645ee3f41c81f3;hpb=0224ce3e20ff502b7ce04865bc23ed99a47c764d;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index d8d3166dc..f7ca2388c 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -221,14 +221,17 @@ 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 (x,_,_,_) -> 
+	  res := Exception UnexpectedGetterOutput
       | _ -> ());
    match !res with
    | Unknown -> raise UnexpectedGetterOutput
@@ -238,8 +241,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 +264,22 @@ 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)
-
-  (* Warning: this fail if uri is already registered *)
+    (map_of_uri uri)#resolve uri
+	
 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
+    try
+      (map_of_uri uri)#remove uri
+    with Key_not_found _ -> ()
+
 let update ?(logger = fun _ -> ()) () =
   if remote () then
     update_remote logger ()
@@ -282,7 +290,9 @@ let getxml ?(format = `Normal) ?(patch_dtd = true) uri =
   if remote () then
     getxml_remote ~format ~patch_dtd uri
   else begin
+    Http_getter_logger.log ~level:2 ("getxml: " ^ uri);
     let url = resolve uri in
+    Http_getter_logger.log ~level:2 ("resolved_uri: " ^ url) ;
     let (fname, outchan) = temp_file_of_uri uri in
     Http_getter_cache.respond_xml ~via_http:false ~enc:format ~patch:patch_dtd
       ~uri ~url outchan;
@@ -294,6 +304,7 @@ let getxslt ?(patch_dtd = true) uri =
   if remote () then
     getxslt_remote ~patch_dtd uri
   else begin
+    
     let url = resolve uri in
     let (fname, outchan) = temp_file_of_uri uri in
     Http_getter_cache.respond_xsl ~via_http:false ~url ~patch:patch_dtd outchan;
@@ -364,8 +375,8 @@ let getalluris () =
     getalluris_remote ()
   else
     let filter uri =
-      (Pcre.pmatch ~rex:heading_cic_RE uri) &&
-      not (Pcre.pmatch ~rex:trailing_types_RE uri)
+      (Pcre.pmatch ~rex:heading_cic_RE uri)
+(*       && not (Pcre.pmatch ~rex:trailing_types_RE uri) *)
     in
     return_uris (Lazy.force cic_map) filter
 
@@ -480,9 +491,6 @@ let ls =
                  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
@@ -495,10 +503,6 @@ prerr_endline ("### " ^ uri ^ " ==> " ^ !dir_found ^ " ==> " ^ dir);
              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
@@ -522,4 +526,10 @@ prerr_endline ("!!! " ^ String.concat " " (List.map fst !candidates_found));
 let getxml' uri = getxml (UriManager.string_of_uri uri)
 let resolve' uri = resolve (UriManager.string_of_uri uri)
 let register' uri url = register ~uri:(UriManager.string_of_uri uri) ~url
+let init () =
+  Http_getter_logger.set_log_level
+    (Helm_registry.get_opt_default Helm_registry.get_int 1 "getter.log_level");
+  Http_getter_logger.set_log_file
+    (Helm_registry.get_opt Helm_registry.get_string "getter.log_file");
+  Http_getter_env.reload ()