X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter_cache.ml;fp=helm%2Focaml%2Fgetter%2Fhttp_getter_cache.ml;h=0000000000000000000000000000000000000000;hp=144b9ac5f4c5ad99f9ebad8fb528a4977878a3f0;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/getter/http_getter_cache.ml b/helm/ocaml/getter/http_getter_cache.ml deleted file mode 100644 index 144b9ac5f..000000000 --- a/helm/ocaml/getter/http_getter_cache.ml +++ /dev/null @@ -1,248 +0,0 @@ -(* - * Copyright (C) 2003-2004: - * Stefano Zacchiroli - * for the HELM Team http://helm.cs.unibo.it/ - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* TODO cache expires control!!! *) -(* TODO uwobo loop: - if two large proof (already in cache) are requested at the same time by two - clients, uwobo (java implementation, not yet tested with the OCaml one) - starts looping sending output to one of the client *) - -open Http_getter_common -open Http_getter_misc -open Http_getter_types -open Printf - - (* expose ThreadSafe.threadSafe methods *) -class threadSafe = - object - inherit ThreadSafe.threadSafe - method virtual doCritical : 'a. 'a lazy_t -> 'a - method virtual doReader : 'a. 'a lazy_t -> 'a - method virtual doWriter : 'a. 'a lazy_t -> 'a - end - -let threadSafe = new threadSafe - -let finally cleanup f = - try - let res = Lazy.force f in - cleanup (); - res - with e -> - cleanup (); - raise (Http_getter_types.Cache_failure (Printexc.to_string e)) - -let resource_type_of_url = function - | url when Pcre.pmatch ~pat:"\\.xml\\.gz$" url -> `Gzipped - | url when Pcre.pmatch ~pat:"\\.xml$" url -> `Normal - | url -> raise (Invalid_URL url) - -let extension_of_resource_type = function - | `Normal -> "xml" - | `Gzipped -> "xml.gz" - - (* basename = resource name without trailing ".gz", if any *) -let is_in_cache basename = - Sys.file_exists - (match Lazy.force Http_getter_env.cache_mode with - | `Normal -> basename - | `Gzipped -> basename ^ ".gz") - -let respond_xml - ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url ~uri outchan - = - let resource_type = resource_type_of_url url in - let extension = extension_of_resource_type resource_type in - let downloadname = - match uri_of_string uri with (* parse uri *) - | Cic_uri (Cic baseuri) | Cic_uri (Theory baseuri) -> - (* assumption: baseuri starts with "/" *) - sprintf "%s%s.%s" (Lazy.force Http_getter_env.cic_dir) baseuri extension - | Nuprl_uri baseuri -> - (* assumption: baseuri starts with "/" *) - sprintf "%s%s.%s" (Lazy.force Http_getter_env.nuprl_dir) baseuri - extension - | Rdf_uri (prefix, ((Cic baseuri) as qbaseuri)) - | Rdf_uri (prefix, ((Theory baseuri) as qbaseuri)) -> - let escaped_prefix = - (Pcre.replace ~pat:"/" ~templ:"_" - (Pcre.replace ~pat:"_" ~templ:"__" - (prefix ^ - (match qbaseuri with - | Cic _ -> "//cic:" - | Theory _ -> "//theory:")))) - in - sprintf "%s/%s%s.%s" - (Lazy.force Http_getter_env.rdf_dir) escaped_prefix baseuri extension - in - let patch_fun = - let xmlbases = - if Http_getter_common.is_theory_uri uri then - Some (Filename.dirname uri, Filename.dirname url) - else - None - in - if patch then - Http_getter_common.patch_xml ?xmlbases ~via_http () - else - (fun x -> x) - in - let basename = Pcre.replace ~pat:"\\.gz$" downloadname in - let contype = "text/xml" in - (* Fill cache if needed and return a short circuit file. - Short circuit is needed in situations like: - resource type = normal, cache type = gzipped, required encoding = normal - we would like to avoid normal -> gzipped -> normal conversions. To avoid - this tmp_short_circuit is used to remember the name of the intermediate - file name *) - let fill_cache () = - threadSafe#doWriter (lazy( - 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 - | `Normal, `Normal | `Gzipped, `Gzipped -> - wget ~output:downloadname url; - None - | `Normal, `Gzipped -> (* resource normal, cache gzipped *) - let tmp = tempfile () in - let (res, cleanup) = - if enc = `Normal then (* user wants normal: don't delete it! *) - (Some (tmp, enc), (fun () -> ())) - else - (None, (fun () -> Sys.remove tmp)) - in - finally cleanup (lazy ( - wget ~output:tmp url; - gzip ~output:(basename ^ ".gz") ~keep:true tmp; (* fill cache *) - res - )); - | `Gzipped, `Normal -> (* resource gzipped, cache normal *) - let tmp = tempfile () in - let (res, cleanup) = - if enc = `Gzipped then (* user wants .gz: don't delete it! *) - (Some (tmp, enc), (fun () -> ())) - else - (None, (fun () -> Sys.remove tmp)) - in - finally cleanup (lazy ( - wget ~output:tmp url; - gunzip ~output:basename ~keep:true tmp; (* fill cache *) - res - )); - end else begin - 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 - | `Normal, `Normal | `Gzipped, `Gzipped -> - (* resource in cache 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 - | `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 - 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"; - let tmp = tempfile () in - finally (fun () -> Sys.remove tmp) (lazy ( - (match enc with - | `Normal -> - (* required format is normal, cached version is gzipped *) - gunzip (* gunzip to tmp *) - ~output:tmp ~keep:true (basename ^ ".gz"); - return_file ~via_http ~fname:tmp ~contype ~patch_fun 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 - 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 - )) - | 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 - ))) - )) - - (* TODO enc is not yet supported *) -let respond_xsl - ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url outchan - = - let patch_fun = - if patch then Http_getter_common.patch_xsl ~via_http () else (fun x -> x) - in - 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 - )) - - (* TODO enc is not yet supported *) -let respond_dtd - ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url outchan - = - let patch_fun = - if patch then Http_getter_common.patch_dtd ~via_http () else (fun x -> x) - 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 - else - raise (Dtd_not_found url) - -let clean () = - let module E = Http_getter_env in - List.iter - (function dir -> ignore (Unix.system ("rm -rf " ^ dir ^ "/*"))) - [ Lazy.force E.cic_dir; Lazy.force E.nuprl_dir; Lazy.force E.rdf_dir ] -