]> matita.cs.unibo.it Git - helm.git/blob - helm/http_getter/http_getter_cache.ml
- fixed helm web page url and copyright notice
[helm.git] / helm / http_getter / http_getter_cache.ml
1 (*
2  * Copyright (C) 2003:
3  *    Stefano Zacchiroli <zack@cs.unibo.it>
4  *    for the HELM Team http://helm.cs.unibo.it/
5  *
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.
9  *
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.
14  *
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.
19  *
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,
23  *  MA  02111-1307, USA.
24  *
25  *  For details, see the HELM World-Wide-Web page,
26  *  http://helm.cs.unibo.it/
27  *)
28
29 open Http_getter_common;;
30 open Http_getter_misc;;
31 open Http_getter_types;;
32 open Printf;;
33
34 let resource_type_of_url = function
35   | url when Pcre.pmatch ~pat:"\\.xml\\.gz$" url -> Enc_gzipped
36   | url when Pcre.pmatch ~pat:"\\.xml$" url -> Enc_normal
37   | url -> raise (Http_getter_invalid_URL url)
38 let extension_of_resource_type = function
39   | Enc_normal -> "xml"
40   | Enc_gzipped -> "xml.gz"
41
42   (* basename = resource name without trailing ".gz", if any *)
43 let is_in_cache basename =
44   Sys.file_exists
45     (match Http_getter_env.cache_mode with
46     | Enc_normal -> basename
47     | Enc_gzipped -> basename ^ ".gz")
48
49 let respond_xml ?(enc = Enc_normal) ?(patch = true) ~url ~uri outchan =
50   let resource_type = resource_type_of_url url in
51   let extension = extension_of_resource_type resource_type in
52   let downloadname =
53     match http_getter_uri_of_string uri with  (* parse uri *)
54     | Xml_uri (Cic baseuri) | Xml_uri (Theory baseuri) ->
55           (* assumption: baseuri starts with "/" *)
56         sprintf "%s%s.%s" Http_getter_env.xml_dir baseuri extension
57     | Rdf_uri (prefix, ((Cic baseuri) as qbaseuri))
58     | Rdf_uri (prefix, ((Theory baseuri) as qbaseuri)) ->
59         let escaped_prefix =
60           (Pcre.replace ~pat:"/" ~templ:"_"
61             (Pcre.replace ~pat:"_" ~templ:"__"
62               (prefix ^
63               (match qbaseuri with
64               | Cic _ -> "//cic:"
65               | Theory _ -> "//theory:"))))
66         in
67         sprintf "%s/%s%s.%s"
68           Http_getter_env.rdf_dir escaped_prefix baseuri extension
69   in
70   let patch_fun =
71     if patch then Http_getter_common.patch_xml else (fun x -> x)
72   in
73   let basename = Pcre.replace ~pat:"\\.gz$" downloadname in
74   if not (is_in_cache basename) then begin (* download and fill cache *)
75     mkdir ~parents:true (Filename.dirname downloadname);
76     wget ~output:downloadname url;
77     match (resource_type, Http_getter_env.cache_mode) with
78     | Enc_normal, Enc_normal ->
79         (if enc = Enc_gzipped then gzip ~keep:true downloadname)
80     | Enc_gzipped, Enc_gzipped ->
81         (if enc = Enc_normal then gunzip ~keep:true downloadname)
82     | Enc_normal, Enc_gzipped -> gzip ~keep:(enc = Enc_normal) downloadname
83     | Enc_gzipped, Enc_normal -> gunzip ~keep:(enc = Enc_gzipped) downloadname
84   end else begin  (* resource already in cache *)
85     match (enc, Http_getter_env.cache_mode) with
86     | Enc_normal, Enc_normal | Enc_gzipped, Enc_gzipped -> ()
87     | Enc_normal, Enc_gzipped -> gunzip ~keep:true (basename ^ ".gz")
88     | Enc_gzipped, Enc_normal -> gzip ~keep:true basename
89   end;  (* now resource is in cache *)
90   (* invariant: file to be sent back to client is available on disk in the
91   format the client likes *)
92   (match enc with  (* send file to client *)
93   | Enc_normal ->
94       return_file ~fname:basename ~contype:"text/xml" ~patch_fun outchan
95   | Enc_gzipped ->
96       return_file
97         ~fname:(basename ^ ".gz") ~contype:"text/xml"  ~contenc:"x-gzip"
98         ~patch_fun outchan);
99   match (enc, Http_getter_env.cache_mode) with  (* remove temp files *)
100   | Enc_normal, Enc_normal | Enc_gzipped, Enc_gzipped -> ()
101   | Enc_normal, Enc_gzipped -> Sys.remove basename
102   | Enc_gzipped, Enc_normal -> Sys.remove (basename ^ ".gz")
103
104   (* TODO enc is not yet supported *)
105 let respond_xsl ?(enc = Enc_normal) ?(patch = true) ~url outchan =
106   let patch_fun =
107     if patch then Http_getter_common.patch_xsl else (fun x -> x)
108   in
109   let fname = tempfile () in
110   wget ~output:fname url;
111   return_file ~fname ~contype:"text/xml" ~patch_fun outchan;
112   Sys.remove fname
113
114   (* TODO enc is not yet supported *)
115 let respond_dtd ?(enc = Enc_normal) ?(patch = true) ~url outchan =
116   let patch_fun =
117     if patch then Http_getter_common.patch_dtd else (fun x -> x)
118   in
119   if Sys.file_exists url then
120     (* TODO check this: old getter here used text/xml *)
121     return_file ~fname:url ~contype:"text/plain" ~patch_fun outchan
122   else
123     return_html_error ("Can't find DTD: " ^ url) outchan
124