From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Feb 2005 09:24:01 +0000 (+0000)
Subject: do not cache local resources (i.e. file:// urls)
X-Git-Tag: V_0_1_0~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d753d75c2270721e58940ba1c347d6371a993683;p=helm.git

do not cache local resources (i.e. file:// urls)
---

diff --git a/helm/ocaml/getter/http_getter_cache.ml b/helm/ocaml/getter/http_getter_cache.ml
index 144b9ac5f..2802f9926 100644
--- a/helm/ocaml/getter/http_getter_cache.ml
+++ b/helm/ocaml/getter/http_getter_cache.ml
@@ -76,6 +76,7 @@ let is_in_cache basename =
 let respond_xml
   ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url ~uri outchan
   =
+  let local_resource = Http_getter_misc.is_local_url url in
   let resource_type = resource_type_of_url url in
   let extension = extension_of_resource_type resource_type in
   let downloadname =
@@ -122,7 +123,10 @@ let respond_xml
       file name *)
   let fill_cache () =
     threadSafe#doWriter (lazy(
-      if not (is_in_cache basename) then begin  (* cache MISS *)
+      if local_resource then begin  (* resource available via file system *)
+        Http_getter_logger.log ~level:2 "Local resource, avoid caching";
+        None
+      end else if not (is_in_cache basename) then begin (* cache miss *)
         Http_getter_logger.log ~level:2 "Cache MISS :-(";
         mkdir ~parents:true (Filename.dirname downloadname);
         match (resource_type, Lazy.force Http_getter_env.cache_mode) with
@@ -155,17 +159,23 @@ let respond_xml
               gunzip ~output:basename ~keep:true tmp; (* fill cache *)
               res
             ));
-      end else begin
+      end else begin  (* cache hit *)
         Http_getter_logger.log ~level:2 "Cache HIT :-)";
         None
       end
     )) in
   let tmp_short_circuit = fill_cache () in
   threadSafe#doReader (lazy(
-    assert (is_in_cache basename);
-    match (enc, Lazy.force Http_getter_env.cache_mode) with
+    assert (local_resource || is_in_cache basename);
+    let resource_type =
+      if local_resource then
+        resource_type
+      else
+        Lazy.force Http_getter_env.cache_mode
+    in
+    match (enc, resource_type) with
     | `Normal, `Normal | `Gzipped, `Gzipped ->
-        (* resource in cache is already in the required format *)
+        (* resource (in cache or local) is already in the required format *)
         (match enc with
         | `Normal ->
             Http_getter_logger.log ~level:2
@@ -182,12 +192,12 @@ let respond_xml
         (match tmp_short_circuit with
         | None -> (* no short circuit possible, use cache *)
           Http_getter_logger.log ~level:2
-            "No short circuit available, use cache";
+            "No short circuit available, use cache (or local resource)";
           let tmp = tempfile () in
           finally (fun () -> Sys.remove tmp) (lazy (
             (match enc with
             | `Normal ->
-              (* required format is normal, cached version is gzipped *)
+              (* required format normal, cached (or local) version gzipped *)
               gunzip  (* gunzip to tmp *)
                 ~output:tmp ~keep:true (basename ^ ".gz");
               return_file ~via_http ~fname:tmp ~contype ~patch_fun outchan;