From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 5 Sep 2005 10:26:09 +0000 (+0000)
Subject: bug fix for IDA: uses remote names (i.e. http://..) when patching xml bases so that... 
X-Git-Tag: V_0_1_2_1~110
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=79722263df3193716bdbc37c35180c84e4027631;p=helm.git

bug fix for IDA: uses remote names (i.e. http://..) when patching xml bases so that external links like images gets valid URIs instead of invalid local ones like /tmp/...
---

diff --git a/helm/http_getter/main.ml b/helm/http_getter/main.ml
index e4cae512c..3117a85c9 100644
--- a/helm/http_getter/main.ml
+++ b/helm/http_getter/main.ml
@@ -271,13 +271,16 @@ let callback (req: Http_types.request) outchan =
     | "/help" -> return_help outchan
     | "/getxml" ->
         let uri = req#param "uri" in
-        let fname = Http_getter.getxml uri in
+        let fname = Http_getter.getxml uri in (* local name, in cache *)
+        let remote_name = Http_getter.resolve uri in (* remote name *)
         let src_enc = if is_gzip fname then `Gzipped else `Normal in
         let enc = parse_enc req in
         let fname, cleanup = convert_file ~from_enc:src_enc ~to_enc:enc fname in
         let contenc = if enc = `Gzipped then Some "x-gzip" else None in
         let patch_fun =
-          if parse_patch req then Some (patch_fun_for uri fname) else None
+          if parse_patch req
+          then Some (patch_fun_for uri remote_name)
+          else None
         in
         let gunzip = (enc = `Gzipped) in
         (try