X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter_cache.ml;fp=helm%2Fhttp_getter%2Fhttp_getter_cache.ml;h=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=d132b69a56b2297e6508a0193cf893ace027fd99;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git diff --git a/helm/http_getter/http_getter_cache.ml b/helm/http_getter/http_getter_cache.ml deleted file mode 100644 index d132b69a5..000000000 --- a/helm/http_getter/http_getter_cache.ml +++ /dev/null @@ -1,138 +0,0 @@ -(* - * Copyright (C) 2003: - * 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 possible race condition, e.g.: - two clients require the same URI which is available in cache compressed, the - getter need to uncompress it, send back to client, and delete the - uncompressed file. Actually the uncompressed file name is the same, a temp - file isn't used. *) -(* TODO possible race condition, e.g.: - two clients require the same URI which is not available in cache, cache - filling operation can collide *) -(* 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;; - -let resource_type_of_url = function - | url when Pcre.pmatch ~pat:"\\.xml\\.gz$" url -> Enc_gzipped - | url when Pcre.pmatch ~pat:"\\.xml$" url -> Enc_normal - | url -> raise (Http_getter_invalid_URL url) -let extension_of_resource_type = function - | Enc_normal -> "xml" - | Enc_gzipped -> "xml.gz" - - (* basename = resource name without trailing ".gz", if any *) -let is_in_cache basename = - Sys.file_exists - (match Http_getter_env.cache_mode with - | Enc_normal -> basename - | Enc_gzipped -> basename ^ ".gz") - -let respond_xml ?(enc = 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 http_getter_uri_of_string uri with (* parse uri *) - | Xml_uri (Cic baseuri) | Xml_uri (Theory baseuri) -> - (* assumption: baseuri starts with "/" *) - sprintf "%s%s.%s" Http_getter_env.xml_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" - Http_getter_env.rdf_dir escaped_prefix baseuri extension - in - let patch_fun = - if patch then Http_getter_common.patch_xml else (fun x -> x) - in - let basename = Pcre.replace ~pat:"\\.gz$" downloadname in - if not (is_in_cache basename) then begin (* download and fill cache *) - mkdir ~parents:true (Filename.dirname downloadname); - wget ~output:downloadname url; - match (resource_type, Http_getter_env.cache_mode) with - | Enc_normal, Enc_normal -> - (if enc = Enc_gzipped then gzip ~keep:true downloadname) - | Enc_gzipped, Enc_gzipped -> - (if enc = Enc_normal then gunzip ~keep:true downloadname) - | Enc_normal, Enc_gzipped -> gzip ~keep:(enc = Enc_normal) downloadname - | Enc_gzipped, Enc_normal -> gunzip ~keep:(enc = Enc_gzipped) downloadname - end else begin (* resource already in cache *) - match (enc, Http_getter_env.cache_mode) with - | Enc_normal, Enc_normal | Enc_gzipped, Enc_gzipped -> () - | Enc_normal, Enc_gzipped -> gunzip ~keep:true (basename ^ ".gz") - | Enc_gzipped, Enc_normal -> gzip ~keep:true basename - end; (* now resource is in cache *) - (* invariant: file to be sent back to client is available on disk in the - format the client likes *) - (match enc with (* send file to client *) - | Enc_normal -> - return_file ~fname:basename ~contype:"text/xml" ~patch_fun outchan - | Enc_gzipped -> - return_file - ~fname:(basename ^ ".gz") ~contype:"text/xml" ~contenc:"x-gzip" - ~patch_fun outchan); - match (enc, Http_getter_env.cache_mode) with (* remove temp files *) - | Enc_normal, Enc_normal | Enc_gzipped, Enc_gzipped -> () - | Enc_normal, Enc_gzipped -> Sys.remove basename - | Enc_gzipped, Enc_normal -> Sys.remove (basename ^ ".gz") - - (* TODO enc is not yet supported *) -let respond_xsl ?(enc = Enc_normal) ?(patch = true) ~url outchan = - let patch_fun = - if patch then Http_getter_common.patch_xsl else (fun x -> x) - in - let fname = tempfile () in - wget ~output:fname url; - return_file ~fname ~contype:"text/xml" ~patch_fun outchan; - Sys.remove fname - - (* TODO enc is not yet supported *) -let respond_dtd ?(enc = Enc_normal) ?(patch = true) ~url outchan = - let patch_fun = - if patch then Http_getter_common.patch_dtd else (fun x -> x) - in - if Sys.file_exists url then - (* TODO check this: old getter here used text/xml *) - return_file ~fname:url ~contype:"text/plain" ~patch_fun outchan - else - return_html_error ("Can't find DTD: " ^ url) outchan -