]> matita.cs.unibo.it Git - helm.git/blob - helm/http_getter/main.ml
split into two major parts:
[helm.git] / helm / http_getter / main.ml
1 (*
2  * Copyright (C) 2003-2004:
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 Printf
30
31 open Http_getter_common
32 open Http_getter_misc
33 open Http_getter_types
34 open Http_getter_debugger
35
36   (* constants *)
37
38 let common_headers = [
39   "Cache-Control", "no-cache";
40   "Pragma", "no-cache";
41   "Expires", "0"
42 ]
43
44   (* HTTP queries argument parsing *)
45
46   (* parse encoding ("format" parameter), default is Enc_normal *)
47 let parse_enc (req: Http_types.request) =
48   try
49     (match req#param "format" with
50     | "normal" -> Enc_normal
51     | "gz" -> Enc_gzipped
52     | s -> raise (Bad_request ("Invalid format: " ^ s)))
53   with Http_types.Param_not_found _ -> Enc_normal
54
55   (* parse "patch_dtd" parameter, default is true *)
56 let parse_patch (req: Http_types.request) =
57   try
58     (match req#param "patch_dtd" with
59     | s when String.lowercase s = "yes" -> true
60     | s when String.lowercase s = "no" -> false
61     | s -> raise (Bad_request ("Invalid patch_dtd value: " ^ s)))
62   with Http_types.Param_not_found _ -> true
63
64   (* parse output format ("format" parameter), no default value *)
65 let parse_output_format (req: Http_types.request) =
66   match req#param "format" with
67   | s when String.lowercase s = "txt" -> Fmt_text
68   | s when String.lowercase s = "xml" -> Fmt_xml
69   | s -> raise (Bad_request ("Invalid /ls format: " ^ s))
70
71   (* parse "baseuri" format for /ls method, no default value *)
72 let parse_ls_uri =
73   let parse_ls_RE = Pcre.regexp "^(\\w+):(.*)$" in
74   let trailing_slash_RE = Pcre.regexp "/+$" in
75   let wrong_uri uri =
76     raise (Bad_request ("Invalid /ls baseuri: " ^ uri))
77   in
78   fun (req: Http_types.request) ->
79     let baseuri = req#param "baseuri" in
80     try
81       let subs =
82         Pcre.extract ~rex:parse_ls_RE
83           (Pcre.replace ~rex:trailing_slash_RE  baseuri)
84       in
85       (match (subs.(1), subs.(2)) with
86       | "cic", uri -> Cic uri
87       | "theory", uri -> Theory uri
88       | _ -> wrong_uri baseuri)
89     with Not_found -> wrong_uri baseuri
90
91   (* parse "position" argument, default is 0 *)
92 let parse_position (req: Http_types.request) =
93   try
94     let res = int_of_string (req#param "position") in
95     if res < 0 then
96       raise (Failure "int_of_string");
97     res
98   with
99   | Http_types.Param_not_found _ -> 0
100   | Failure "int_of_string" ->
101     raise (Bad_request
102       (sprintf "position must be a non negative integer (%s given)"
103         (req#param "position")))
104
105 let parse_rdf_class (req: Http_types.request) =
106   match req#param "class" with
107   | "forward" -> `Forward
108   | "backward" -> `Backward
109   | c -> raise (Bad_request ("Invalid RDF class: " ^ c))
110
111 let return_all_foo_uris doctype uris outchan =
112   Http_daemon.send_basic_headers ~code:200 outchan;
113   Http_daemon.send_header "Content-Type" "text/xml" outchan;
114   Http_daemon.send_headers common_headers outchan;
115   Http_daemon.send_CRLF outchan;
116   output_string
117     outchan
118     (sprintf
119 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>
120 <!DOCTYPE %s SYSTEM \"%s/getdtd?uri=%s.dtd\">
121
122 <%s>
123 "
124       doctype
125       Http_getter_env.my_own_url
126       doctype
127       doctype);
128   List.iter
129     (fun uri -> output_string outchan (sprintf "\t<uri value=\"%s\" />\n" uri))
130     uris;
131   output_string outchan (sprintf "</%s>\n" doctype)
132
133 let return_all_xml_uris outchan =
134   return_all_foo_uris "alluris" (Http_getter.getalluris ()) outchan
135 let return_all_rdf_uris classs outchan =
136   return_all_foo_uris "allrdfuris" (Http_getter.getallrdfuris classs) outchan
137
138 let return_ls xmluri fmt outchan =
139   let ls_items = Http_getter.ls xmluri in
140   let buf = Buffer.create 10240 in
141   (match fmt with
142   | Fmt_text ->
143       List.iter
144         (function
145           | Ls_section dir -> bprintf buf "dir, %s\n" dir
146           | Ls_object obj ->
147               bprintf buf "object, %s, <%s,%s,%s,%s>\n"
148               obj.uri (if obj.ann then "YES" else "NO")
149               (string_of_ls_flag obj.types)
150               (string_of_ls_flag obj.body)
151               (string_of_ls_flag obj.proof_tree))
152         ls_items
153   | Fmt_xml ->
154       Buffer.add_string buf "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
155       bprintf buf "<!DOCTYPE ls SYSTEM \"%s/getdtd?uri=ls.dtd\">\n"
156         Http_getter_env.my_own_url;
157       Buffer.add_string buf "<ls>\n";
158       List.iter
159         (function
160           | Ls_section dir -> bprintf buf "<section>%s</section>\n" dir
161           | Ls_object obj ->
162               bprintf buf
163 "<object name=\"%s\">
164 \t<ann value=\"%s\" />
165 \t<types value=\"%s\" />
166 \t<body value=\"%s\" />
167 \t<proof_tree value=\"%s\" />
168 </object>
169 "
170               obj.uri (if obj.ann then "YES" else "NO")
171               (string_of_ls_flag obj.types)
172               (string_of_ls_flag obj.body)
173               (string_of_ls_flag obj.proof_tree))
174         ls_items;
175       Buffer.add_string buf "</ls>\n");
176   let body = Buffer.contents buf in
177   Http_daemon.respond
178     ~headers:(("Content-Type", "text/plain") :: common_headers)
179     ~body outchan
180
181 let return_help outchan = return_html_raw (Http_getter.help ()) outchan
182
183 let return_resolve uri outchan =
184   try
185     return_xml_raw
186       (sprintf "<url value=\"%s\" />\n" (Http_getter.resolve uri))
187       outchan
188   with Unresolvable_URI uri ->
189     return_xml_raw "<unresolved />\n" outchan
190
191 let return_list_servers outchan =
192   return_html_raw
193     (sprintf "<html><body><table>\n%s\n</table></body></html>"
194       (String.concat "\n"
195         (List.map
196           (fun (pos, server) ->
197             sprintf "<tr><td>%d</td><td>%s</td></tr>" pos server)
198           (Http_getter.list_servers ()))))
199     outchan
200
201   (* thread action *)
202
203 let callback (req: Http_types.request) outchan =
204   try
205     debug_print ("Connection from " ^ req#clientAddr);
206     debug_print ("Received request: " ^ req#path);
207     (match req#path with
208     | "/help" -> return_help outchan
209     | "/getxml" ->
210         let uri = req#param "uri" in
211         Http_getter_cache.respond_xml ~url:(Http_getter.resolve uri) ~uri
212           ~enc:(parse_enc req) ~patch:(parse_patch req) outchan
213     | "/getxslt" ->
214         Http_getter_cache.respond_xsl
215           ~url:(Http_getter.resolve (req#param "uri"))
216           ~patch:(parse_patch req) outchan
217     | "/getdtd" ->
218         Http_getter_cache.respond_dtd ~patch:(parse_patch req)
219           ~url:(Http_getter_env.dtd_dir ^ "/" ^ (req#param "uri")) outchan
220     | "/resolve" -> return_resolve (req#param "uri") outchan
221     | "/register" ->
222         Http_getter.register ~uri:(req#param "uri") ~url:(req#param "url");
223         return_html_msg "Register done" outchan
224     | "/clean_cache" ->
225         Http_getter.clean_cache ();
226         return_html_msg "Done." outchan
227     | "/update" ->
228         Http_getter_env.reload (); (* reload servers list from servers file *)
229         let log = Http_getter.update () in
230         return_html_msg (Ui_logger.html_of_html_msg log) outchan
231     | "/list_servers" -> return_list_servers outchan
232     | "/add_server" ->
233         let name = req#param "url" in
234         let position = parse_position req in
235         let log = Http_getter.add_server ~position name in
236         return_html_msg
237           (sprintf "Added server %s in position %d)<br />\n%s"
238             name position (Ui_logger.html_of_html_msg log))
239           outchan
240     | "/remove_server" ->
241         let position = parse_position req in
242         let log =
243           try
244             Http_getter.remove_server position
245           with Invalid_argument _ ->
246             raise (Bad_request (sprintf "no server with position %d" position))
247         in
248         return_html_msg
249           (sprintf "Removed server at position %d<br />\n%s"
250             position (Ui_logger.html_of_html_msg log))
251           outchan
252     | "/getalluris" -> return_all_xml_uris outchan
253     | "/getallrdfuris" -> return_all_rdf_uris (parse_rdf_class req) outchan
254     | "/ls" -> return_ls (parse_ls_uri req) (parse_output_format req) outchan
255     | "/getempty" ->
256         Http_daemon.respond ~body:Http_getter_const.empty_xml outchan
257     | invalid_request ->
258         Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
259     debug_print "Done!\n"
260   with
261   | Http_types.Param_not_found attr_name ->
262       return_400 (sprintf "Parameter '%s' is missing" attr_name) outchan
263   | Bad_request msg -> return_html_error msg outchan
264   | Internal_error msg -> return_html_internal_error msg outchan
265   | Shell.Subprocess_error l ->
266       return_html_internal_error
267         (String.concat "<br />\n"
268           (List.map
269             (fun (cmd, code) ->
270               sprintf "Command '%s' returned %s"
271                 cmd (string_of_proc_status code))
272             l))
273         outchan
274   | exc ->
275       return_html_error
276         ("Uncaught exception: " ^ (Printexc.to_string exc))
277         outchan
278
279     (* Main *)
280
281 let main () =
282   print_string (Http_getter_env.env_to_string ());
283   flush stdout;
284   at_exit Http_getter.close_maps;
285   Sys.catch_break true;
286   try
287     Http_daemon.start'
288       ~timeout:(Some 600) ~port:Http_getter_env.port ~mode:`Thread callback
289   with Sys.Break -> ()  (* 'close_maps' already registered with 'at_exit' *)
290
291 let _ = main ()
292