X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fpxp%2FpxpUrlResolver.ml;h=ec94b4e5ee4d2c7e6a4b46fd57acebd1fd7fa7d9;hb=cc6e7ad571d40a88686427bd75e0fa38c0fa120b;hp=89d540e62fcb0b58c2ad388ae259f4bda95c58d5;hpb=be4d9c44f4d9df070339da40aa82c8cb0cc6467c;p=helm.git

diff --git a/helm/ocaml/pxp/pxpUrlResolver.ml b/helm/ocaml/pxp/pxpUrlResolver.ml
index 89d540e62..ec94b4e5e 100644
--- a/helm/ocaml/pxp/pxpUrlResolver.ml
+++ b/helm/ocaml/pxp/pxpUrlResolver.ml
@@ -23,7 +23,47 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* This resolver uses ClientHTTP to download the files from the Web *)
+(* cut and paste from ../getter/clientHTTP.ml *)
+exception HttpClientError of string * string;;	(* reason, uri *)
+
+let send cmd =
+ try
+  ignore (Http_client.http_get cmd)
+ with
+  e -> raise (HttpClientError (Printexc.to_string e, cmd))
+;;
+
+let get uri =
+ try
+  Http_client.http_get uri
+ with
+  e -> raise (HttpClientError (Printexc.to_string e, uri))
+;;
+
+let get_and_save uri dest_filename =
+ let reply = get uri
+ and out_channel = open_out dest_filename in
+  output_string out_channel reply ;
+  close_out out_channel
+;;
+
+let get_and_save_to_tmp uri =
+ let flat_string s s' c =
+  let cs = String.copy s in
+   for i = 0 to (String.length s) - 1 do
+    if String.contains s' s.[i] then cs.[i] <- c
+   done ;
+   cs
+ in
+  let user = try Unix.getlogin () with _ -> "" in
+  let tmp_file =
+    Filename.temp_file (user ^ flat_string uri ".-=:;!?/&" '_') ""
+  in
+  get_and_save uri tmp_file ;
+  tmp_file
+;;
+(* / cut and paste from ../getter/clientHTTP.ml *)
+
 let url_resolver =
  let url_of_id =
   function
@@ -33,7 +73,7 @@ let url_resolver =
    | _ -> raise Pxp_reader.Not_competent
  in
  let channel_of_url _ url =
-  let file = ClientHTTP.get_and_save_to_tmp (Neturl.string_of_url url) in
+  let file = get_and_save_to_tmp (Neturl.string_of_url url) in
   let ch = open_in file in
    Unix.unlink file ;
    ch,None
@@ -41,3 +81,4 @@ let url_resolver =
   new Pxp_reader.resolve_read_url_channel
    ~url_of_id ~channel_of_url ()
 ;;
+