]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/http_getter_cache.ml
prima implementazione di demodulate, superposition_left e superposition_right
[helm.git] / helm / ocaml / getter / http_getter_cache.ml
index ef0a8dffa6b5e904efe7466250ee70b593b94b54..e6627fa1e3ddab95761eba19c3b407e75cab8a92 100644 (file)
@@ -76,6 +76,8 @@ let is_in_cache basename =
 let respond_xml
   ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url ~uri outchan
   =
+  let local_part = Http_getter_misc.local_url url in
+  let local_resource = local_part <> None in
   let resource_type = resource_type_of_url url in
   let extension = extension_of_resource_type resource_type in
   let downloadname =
@@ -101,10 +103,16 @@ let respond_xml
           (Lazy.force Http_getter_env.rdf_dir) escaped_prefix baseuri extension
   in
   let patch_fun =
-    if patch then
-      Http_getter_common.patch_xml ~xmlbases:(uri, url) ~via_http ()
-    else
-      (fun x -> x)
+    let xmlbases =
+     if Http_getter_common.is_theory_uri uri then
+      Some (Filename.dirname uri, Filename.dirname url)
+     else
+      None
+    in
+     if patch then
+       Some (Http_getter_common.patch_xml ?xmlbases ~via_http ())
+     else
+       None
   in
   let basename = Pcre.replace ~pat:"\\.gz$" downloadname in
   let contype = "text/xml" in
@@ -116,7 +124,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
@@ -149,62 +160,70 @@ 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 basename = match local_part with Some f -> f | None -> basename in
+    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
               "No format mangling required (encoding = normal)";
-            return_file ~via_http ~fname:basename ~contype ~patch_fun outchan
+            return_file ~via_http ~fname:basename ~contype ?patch_fun ~enc
+              outchan
         | `Gzipped ->
             Http_getter_logger.log ~level:2
               "No format mangling required (encoding = gzipped)";
             return_file
               ~via_http ~fname:(basename ^ ".gz") ~contype ~contenc:"x-gzip"
-              ~patch_fun ~gunzip:true
+              ?patch_fun ~gunzip:true ~enc
               outchan)
     | `Normal, `Gzipped | `Gzipped, `Normal ->
         (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;
+              return_file ~via_http ~fname:tmp ~contype ?patch_fun ~enc outchan
             | `Gzipped ->
               (* required format is gzipped, cached version is normal *)
               gzip ~output:tmp ~keep:true basename;  (* gzip to tmp *)
               return_file
                 ~via_http ~fname:tmp ~contype ~contenc:"x-gzip"
-                ~patch_fun ~gunzip:true
+                ?patch_fun ~gunzip:true ~enc
                 outchan)
           ))
         | Some (fname, `Normal) ->  (* short circuit available, use it! *)
             Http_getter_logger.log ~level:2
               "Using short circuit (encoding = normal)";
             finally (fun () -> Sys.remove fname) (lazy (
-              return_file ~via_http ~fname ~contype ~patch_fun outchan
+              return_file ~via_http ~fname ~contype ?patch_fun ~enc outchan
             ))
         | Some (fname, `Gzipped) -> (* short circuit available, use it! *)
             Http_getter_logger.log ~level:2
               "Using short circuit (encoding = gzipped)";
             finally (fun () -> Sys.remove fname) (lazy (
-              return_file ~via_http ~fname ~contype ~contenc:"x-gzip" ~patch_fun
-                ~gunzip:true outchan
+              return_file ~via_http ~fname ~contype ~contenc:"x-gzip" ?patch_fun
+                ~gunzip:true ~enc outchan
             )))
   ))
 
@@ -218,7 +237,7 @@ let respond_xsl
   let fname = tempfile () in
   finally (fun () -> Sys.remove fname) (lazy (
     wget ~output:fname url;
-    return_file ~via_http ~fname ~contype:"text/xml" ~patch_fun outchan
+    return_file ~via_http ~fname ~contype:"text/xml" ~patch_fun ~enc outchan
   ))
 
   (* TODO enc is not yet supported *)
@@ -230,7 +249,8 @@ let respond_dtd
   in
   if Sys.file_exists url then
     (* TODO check this: old getter here used text/xml *)
-    return_file ~via_http ~fname:url ~contype:"text/plain" ~patch_fun outchan
+    return_file ~via_http ~fname:url ~contype:"text/plain" ~patch_fun ~enc 
+      outchan
   else
     raise (Dtd_not_found url)