added cast rendering (used in check window by gTopLevel/matita)

[helm.git] / helm / ocaml / getter / http_getter.ml

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index d8d3166dceb7986101afc70d3d645ee3f41c81f3..539fa90a700570b6be85179b8e42513c903c5e8e 100644 (file)
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -77,7 +77,7 @@ let map_of_uri = function
   | uri when is_nuprl_uri uri -> Lazy.force nuprl_map
   | uri when is_rdf_uri uri -> Lazy.force rdf_map
   | uri when is_xsl_uri uri -> Lazy.force xsl_map
-  | uri -> raise (Unresolvable_URI uri)
+  | uri -> prerr_endline "BBBBB";raise (Unresolvable_URI uri)
 
 let update_from_server logger server_url = (* use global maps *)
   Http_getter_logger.log ("Updating information from " ^ server_url);
@@ -221,25 +221,33 @@ 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,_,_,_) -> 
+         prerr_endline ("UnexpectedGetterOutput: "^x);
+         res := Exception UnexpectedGetterOutput
       | _ -> ());
    match !res with
-   | Unknown -> raise UnexpectedGetterOutput
-   | Exception e -> raise e
+   | Unknown -> 
+       prerr_endline ("UnexpectedGetterOutput: Unknown!");
+       raise UnexpectedGetterOutput
+   | Exception e -> 
+       prerr_endline ("Exception   : ??????");
+       raise e
    | Resolved url -> url
 
 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 +269,29 @@ let resolve uri =
   if remote () then
     resolve_remote uri
   else
-    try
+    
+    (**** FIXME ******)
+    if is_cic_uri uri && Pcre.pmatch ~pat:"\\.univ$" uri then
+      begin
+       prerr_endline "!!! E' in ~tassi !!!";
+       "file:///home/tassi/mylib" ^ 
+       (String.sub uri 4 ((String.length uri) - 4)) ^ ".xml.gz"
+      end
+    else
       (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 *)
+       
 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 ()
@@ -282,7 +302,9 @@ let getxml ?(format = `Normal) ?(patch_dtd = true) uri =
   if remote () then
     getxml_remote ~format ~patch_dtd uri
   else begin
+Http_getter_logger.log ("GETXML: " ^ uri);
     let url = resolve uri in
+Http_getter_logger.log ("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 +316,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;