(* * Copyright (C) 2003-2004: * 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/ *) open Printf open Http_getter_common open Http_getter_misc open Http_getter_types open Http_getter_debugger (* constants *) let configuration_file = "http_getter.conf.xml" let common_headers = [ "Cache-Control", "no-cache"; "Pragma", "no-cache"; "Expires", "0" ] (* HTTP queries argument parsing *) (* parse encoding ("format" parameter), default is Enc_normal *) let parse_enc (req: Http_types.request) = try (match req#param "format" with | "normal" -> Enc_normal | "gz" -> Enc_gzipped | s -> raise (Bad_request ("Invalid format: " ^ s))) with Http_types.Param_not_found _ -> Enc_normal (* parse "patch_dtd" parameter, default is true *) let parse_patch (req: Http_types.request) = try (match req#param "patch_dtd" with | s when String.lowercase s = "yes" -> true | s when String.lowercase s = "no" -> false | s -> raise (Bad_request ("Invalid patch_dtd value: " ^ s))) with Http_types.Param_not_found _ -> true (* parse output format ("format" parameter), no default value *) let parse_output_format meth (req: Http_types.request) = match req#param "format" with | s when String.lowercase s = "txt" -> Fmt_text | s when String.lowercase s = "xml" -> Fmt_xml | s -> raise (Bad_request ("Invalid /" ^ meth ^ " format: " ^ s)) (* parse "baseuri" format for /ls method, no default value *) let parse_ls_uri = let parse_ls_RE = Pcre.regexp "^(\\w+):(.*)$" in let trailing_slash_RE = Pcre.regexp "/+$" in let wrong_uri uri = raise (Bad_request ("Invalid /ls baseuri: " ^ uri)) in fun (req: Http_types.request) -> let baseuri = req#param "baseuri" in try let subs = Pcre.extract ~rex:parse_ls_RE (Pcre.replace ~rex:trailing_slash_RE baseuri) in (match (subs.(1), subs.(2)) with | "cic", uri -> Cic uri | "theory", uri -> Theory uri | _ -> wrong_uri baseuri) with Not_found -> wrong_uri baseuri (* parse "position" argument, default is 0 *) let parse_position (req: Http_types.request) = try let res = int_of_string (req#param "position") in if res < 0 then raise (Failure "int_of_string"); res with | Http_types.Param_not_found _ -> 0 | Failure "int_of_string" -> raise (Bad_request (sprintf "position must be a non negative integer (%s given)" (req#param "position"))) let parse_rdf_class (req: Http_types.request) = match req#param "class" with | "forward" -> `Forward | "backward" -> `Backward | c -> raise (Bad_request ("Invalid RDF class: " ^ c)) let mk_return_fun pp_fun contype msg outchan = Http_daemon.respond ~body:(pp_fun msg) ~headers:["Content-Type", contype] outchan let pp_error s = sprintf "Http Getter error: %s" s let pp_internal_error s = sprintf "Http Getter Internal error: %s" s let pp_msg s = sprintf "%s" s let null_pp s = s let return_html_error = mk_return_fun pp_error "text/html" let return_html_internal_error = mk_return_fun pp_internal_error "text/html" let return_html_msg = mk_return_fun pp_msg "text/html" let return_html_raw = mk_return_fun null_pp "text/html" let return_xml_raw = mk_return_fun null_pp "text/xml" let return_400 body outchan = Http_daemon.respond_error ~code:400 ~body outchan let return_all_foo_uris doctype uris outchan = Http_daemon.send_basic_headers ~code:200 outchan; Http_daemon.send_header "Content-Type" "text/xml" outchan; Http_daemon.send_headers common_headers outchan; Http_daemon.send_CRLF outchan; output_string outchan (sprintf " <%s> " doctype (Lazy.force Http_getter_env.my_own_url) doctype doctype); List.iter (fun uri -> output_string outchan (sprintf "\t\n" uri)) uris; output_string outchan (sprintf "\n" doctype) let return_all_xml_uris fmt outchan = let uris = Http_getter.getalluris () in match fmt with | Fmt_text -> let buf = Buffer.create 10240 in List.iter (bprintf buf "%s\n") uris ; let body = Buffer.contents buf in Http_daemon.respond ~headers:(("Content-Type", "text/plain") :: common_headers) ~body outchan | Fmt_xml -> return_all_foo_uris "alluris" uris outchan let return_all_rdf_uris classs outchan = return_all_foo_uris "allrdfuris" (Http_getter.getallrdfuris classs) outchan let return_ls xmluri fmt outchan = let ls_items = Http_getter.ls xmluri in let buf = Buffer.create 10240 in (match fmt with | Fmt_text -> List.iter (function | Ls_section dir -> bprintf buf "dir, %s\n" dir | Ls_object obj -> bprintf buf "object, %s, <%s,%s,%s,%s>\n" obj.uri (if obj.ann then "YES" else "NO") (string_of_ls_flag obj.types) (string_of_ls_flag obj.body) (string_of_ls_flag obj.proof_tree)) ls_items | Fmt_xml -> Buffer.add_string buf "\n"; bprintf buf "\n" (Lazy.force Http_getter_env.my_own_url); Buffer.add_string buf "\n"; List.iter (function | Ls_section dir -> bprintf buf "

\n" dir | Ls_object obj -> bprintf buf "

" obj.uri (if obj.ann then "YES" else "NO") (string_of_ls_flag obj.types) (string_of_ls_flag obj.body) (string_of_ls_flag obj.proof_tree)) ls_items; Buffer.add_string buf "\n"); let body = Buffer.contents buf in Http_daemon.respond ~headers:(("Content-Type", "text/plain") :: common_headers) ~body outchan let return_help outchan = return_html_raw (Http_getter.help ()) outchan let return_resolve uri outchan = try return_xml_raw (sprintf "\n" (Http_getter.resolve uri)) outchan with Unresolvable_URI uri -> return_xml_raw "\n" outchan let return_list_servers outchan = return_html_raw (sprintf "\n%s\n

" (String.concat "\n" (List.map (fun (pos, server) -> sprintf "%d%s" pos server) (Http_getter.list_servers ())))) outchan let log_failure msg = debug_print ("Request not fulfilled: " ^ msg) (** given an action (i.e. a function which expects a logger and do something * using it as a logger), perform it sending its output incrementally to the * given output channel. Response is sent embedded in an HTML document. * Channel is closed afterwards. *) let send_log_to ?prepend action outchan = Http_daemon.send_basic_headers ~code:200 outchan; Http_daemon.send_header "Content-Type" "text/html" outchan; Http_daemon.send_CRLF outchan; output_string outchan "\n"; flush outchan; (match prepend with | None -> () | Some text -> output_string outchan text; flush outchan); let logger tag = output_string outchan (HelmLogger.html_of_html_tag tag); flush outchan in action logger; output_string outchan "\n"; close_out outchan (* thread action *) let callback (req: Http_types.request) outchan = try debug_print ("Connection from " ^ req#clientAddr); debug_print ("Received request: " ^ req#path); (match req#path with | "/help" -> return_help outchan | "/getxml" -> let uri = req#param "uri" in Http_getter_cache.respond_xml ~url:(Http_getter.resolve uri) ~uri ~enc:(parse_enc req) ~patch:(parse_patch req) outchan | "/getxslt" -> Http_getter_cache.respond_xsl ~url:(Http_getter.resolve (req#param "uri")) ~patch:(parse_patch req) outchan | "/getdtd" -> Http_getter_cache.respond_dtd ~patch:(parse_patch req) ~url:(sprintf "%s/%s" (Helm_registry.get "getter.dtd_dir") (req#param "uri")) outchan | "/resolve" -> return_resolve (req#param "uri") outchan | "/register" -> Http_getter.register ~uri:(req#param "uri") ~url:(req#param "url"); return_html_msg "Register done" outchan | "/clean_cache" -> Http_getter.clean_cache (); return_html_msg "Done." outchan | "/update" -> Http_getter_env.reload (); (* reload servers list from servers file *) send_log_to (fun logger -> Http_getter.update ~logger ()) outchan | "/list_servers" -> return_list_servers outchan | "/add_server" -> let name = req#param "url" in let position = parse_position req in let prepend = sprintf "Added server %s in position %d)
\n" name position in send_log_to ~prepend (fun logger -> Http_getter.add_server ~logger ~position name) outchan | "/remove_server" -> let position = parse_position req in if not (Http_getter.has_server position) then raise (Bad_request (sprintf "no server with position %d" position)) else let prepend = sprintf "Removed server at position %d
\n" position in send_log_to ~prepend (fun logger -> Http_getter.remove_server ~logger position) outchan | "/getalluris" -> return_all_xml_uris (parse_output_format "getalluris" req) outchan | "/getallrdfuris" -> return_all_rdf_uris (parse_rdf_class req) outchan | "/ls" -> return_ls (parse_ls_uri req) (parse_output_format "ls" req) outchan | "/getempty" -> Http_daemon.respond ~body:Http_getter_const.empty_xml outchan | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); debug_print "Done!\n" with | Http_types.Param_not_found attr_name -> let msg = sprintf "Parameter '%s' is missing" attr_name in log_failure msg; return_400 msg outchan | Bad_request msg -> log_failure msg; return_html_error msg outchan | Internal_error msg -> log_failure msg; return_html_internal_error msg outchan | Shell.Subprocess_error l -> let msgs = List.map (fun (cmd, code) -> sprintf "Command '%s' returned %s" cmd (string_of_proc_status code)) l in log_failure (String.concat ", " msgs); return_html_internal_error (String.concat "
\n" msgs) outchan | exc -> let msg = "Uncaught exception: " ^ (Printexc.to_string exc) in log_failure msg; return_html_error msg outchan (* Main *) let main () = Helm_registry.load_from configuration_file; Http_getter_env.reload (); print_string (Http_getter_env.env_to_string ()); flush stdout; at_exit Http_getter.close_maps; Sys.catch_break true; try Http_daemon.start' ~mode:`Thread ~timeout:(Some 600) ~port:(Helm_registry.get_int "getter.port") callback with Sys.Break -> () (* 'close_maps' already registered with 'at_exit' *) let _ = main ()