+++ /dev/null
-(*
- * Copyright (C) 2003:
- * Stefano Zacchiroli <zack@cs.unibo.it>
- * 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
-
projects / helm.git / blobdiff