3 * Stefano Zacchiroli <zack@cs.unibo.it>
4 * for the HELM Team http://helm.cs.unibo.it/
6 * This file is part of HELM, an Hypertextual, Electronic
7 * Library of Mathematics, developed at the Computer Science
8 * Department, University of Bologna, Italy.
10 * HELM is free software; you can redistribute it and/or
11 * modify it under the terms of the GNU General Public License
12 * as published by the Free Software Foundation; either version 2
13 * of the License, or (at your option) any later version.
15 * HELM is distributed in the hope that it will be useful,
16 * but WITHOUT ANY WARRANTY; without even the implied warranty of
17 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
18 * GNU General Public License for more details.
20 * You should have received a copy of the GNU General Public License
21 * along with HELM; if not, write to the Free Software
22 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
25 * For details, see the HELM World-Wide-Web page,
26 * http://helm.cs.unibo.it/
29 (* TODO cache expires control!!! *)
30 (* TODO possible race condition, e.g.:
31 two clients require the same URI which is available in cache compressed, the
32 getter need to uncompress it, send back to client, and delete the
33 uncompressed file. Actually the uncompressed file name is the same, a temp
35 (* TODO possible race condition, e.g.:
36 two clients require the same URI which is not available in cache, cache
37 filling operation can collide *)
39 if two large proof (already in cache) are requested at the same time by two
40 clients, uwobo (java implementation, not yet tested with the OCaml one)
41 starts looping sending output to one of the client *)
43 open Http_getter_common;;
44 open Http_getter_misc;;
45 open Http_getter_types;;
48 let resource_type_of_url = function
49 | url when Pcre.pmatch ~pat:"\\.xml\\.gz$" url -> Enc_gzipped
50 | url when Pcre.pmatch ~pat:"\\.xml$" url -> Enc_normal
51 | url -> raise (Http_getter_invalid_URL url)
52 let extension_of_resource_type = function
54 | Enc_gzipped -> "xml.gz"
56 (* basename = resource name without trailing ".gz", if any *)
57 let is_in_cache basename =
59 (match Http_getter_env.cache_mode with
60 | Enc_normal -> basename
61 | Enc_gzipped -> basename ^ ".gz")
63 let respond_xml ?(enc = Enc_normal) ?(patch = true) ~url ~uri outchan =
64 let resource_type = resource_type_of_url url in
65 let extension = extension_of_resource_type resource_type in
67 match http_getter_uri_of_string uri with (* parse uri *)
68 | Xml_uri (Cic baseuri) | Xml_uri (Theory baseuri) ->
69 (* assumption: baseuri starts with "/" *)
70 sprintf "%s%s.%s" Http_getter_env.xml_dir baseuri extension
71 | Rdf_uri (prefix, ((Cic baseuri) as qbaseuri))
72 | Rdf_uri (prefix, ((Theory baseuri) as qbaseuri)) ->
74 (Pcre.replace ~pat:"/" ~templ:"_"
75 (Pcre.replace ~pat:"_" ~templ:"__"
79 | Theory _ -> "//theory:"))))
82 Http_getter_env.rdf_dir escaped_prefix baseuri extension
85 if patch then Http_getter_common.patch_xml else (fun x -> x)
87 let basename = Pcre.replace ~pat:"\\.gz$" downloadname in
88 if not (is_in_cache basename) then begin (* download and fill cache *)
89 mkdir ~parents:true (Filename.dirname downloadname);
90 wget ~output:downloadname url;
91 match (resource_type, Http_getter_env.cache_mode) with
92 | Enc_normal, Enc_normal ->
93 (if enc = Enc_gzipped then gzip ~keep:true downloadname)
94 | Enc_gzipped, Enc_gzipped ->
95 (if enc = Enc_normal then gunzip ~keep:true downloadname)
96 | Enc_normal, Enc_gzipped -> gzip ~keep:(enc = Enc_normal) downloadname
97 | Enc_gzipped, Enc_normal -> gunzip ~keep:(enc = Enc_gzipped) downloadname
98 end else begin (* resource already in cache *)
99 match (enc, Http_getter_env.cache_mode) with
100 | Enc_normal, Enc_normal | Enc_gzipped, Enc_gzipped -> ()
101 | Enc_normal, Enc_gzipped -> gunzip ~keep:true (basename ^ ".gz")
102 | Enc_gzipped, Enc_normal -> gzip ~keep:true basename
103 end; (* now resource is in cache *)
104 (* invariant: file to be sent back to client is available on disk in the
105 format the client likes *)
106 (match enc with (* send file to client *)
108 return_file ~fname:basename ~contype:"text/xml" ~patch_fun outchan
111 ~fname:(basename ^ ".gz") ~contype:"text/xml" ~contenc:"x-gzip"
113 match (enc, Http_getter_env.cache_mode) with (* remove temp files *)
114 | Enc_normal, Enc_normal | Enc_gzipped, Enc_gzipped -> ()
115 | Enc_normal, Enc_gzipped -> Sys.remove basename
116 | Enc_gzipped, Enc_normal -> Sys.remove (basename ^ ".gz")
118 (* TODO enc is not yet supported *)
119 let respond_xsl ?(enc = Enc_normal) ?(patch = true) ~url outchan =
121 if patch then Http_getter_common.patch_xsl else (fun x -> x)
123 let fname = tempfile () in
124 wget ~output:fname url;
125 return_file ~fname ~contype:"text/xml" ~patch_fun outchan;
128 (* TODO enc is not yet supported *)
129 let respond_dtd ?(enc = Enc_normal) ?(patch = true) ~url outchan =
131 if patch then Http_getter_common.patch_dtd else (fun x -> x)
133 if Sys.file_exists url then
134 (* TODO check this: old getter here used text/xml *)
135 return_file ~fname:url ~contype:"text/plain" ~patch_fun outchan
137 return_html_error ("Can't find DTD: " ^ url) outchan