X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fmain.ml;h=699c685bb6c56cc840306cc2d84bbe96a02950b6;hb=750e15351055085126b3719e140f96f5f9d41d95;hp=301d74eef4b7d1125a2abf2777d611b9612d4ffa;hpb=3af56c5a48f7cad33fd701e0061fe143e0e2a7c5;p=helm.git diff --git a/helm/http_getter/main.ml b/helm/http_getter/main.ml index 301d74eef..699c685bb 100644 --- a/helm/http_getter/main.ml +++ b/helm/http_getter/main.ml @@ -35,6 +35,7 @@ open Http_getter_debugger (* constants *) +(* let configuration_file = "/projects/helm/etc/http_getter.conf.xml" *) let configuration_file = "http_getter.conf.xml" let common_headers = [ @@ -45,14 +46,14 @@ let common_headers = [ (* HTTP queries argument parsing *) - (* parse encoding ("format" parameter), default is Enc_normal *) + (* parse encoding ("format" parameter), default is `Normal *) let parse_enc (req: Http_types.request) = try (match req#param "format" with - | "normal" -> Enc_normal - | "gz" -> Enc_gzipped + | "normal" -> `Normal + | "gz" -> `Gzipped | s -> raise (Bad_request ("Invalid format: " ^ s))) - with Http_types.Param_not_found _ -> Enc_normal + with Http_types.Param_not_found _ -> `Normal (* parse "patch_dtd" parameter, default is true *) let parse_patch (req: Http_types.request) = @@ -66,8 +67,8 @@ let parse_patch (req: Http_types.request) = (* 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 when String.lowercase s = "txt" -> `Text + | s when String.lowercase s = "xml" -> `Xml | s -> raise (Bad_request ("Invalid /" ^ meth ^ " format: " ^ s)) (* parse "baseuri" format for /ls method, no default value *) @@ -114,9 +115,9 @@ 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 + sprintf "Http Getter error: %s" s let pp_internal_error s = - sprintf "Http Getter Internal error: %s" 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" @@ -151,14 +152,14 @@ let return_all_foo_uris doctype uris outchan = let return_all_xml_uris fmt outchan = let uris = Http_getter.getalluris () in match fmt with - | Fmt_text -> + | `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 -> + | `Xml -> return_all_foo_uris "alluris" uris outchan let return_all_rdf_uris classs outchan = @@ -168,7 +169,7 @@ 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 -> + | `Text -> List.iter (function | Ls_section dir -> bprintf buf "dir, %s\n" dir @@ -179,7 +180,7 @@ let return_ls xmluri fmt outchan = (string_of_ls_flag obj.body) (string_of_ls_flag obj.proof_tree)) ls_items - | Fmt_xml -> + | `Xml -> Buffer.add_string buf "\n"; bprintf buf "\n" (Lazy.force Http_getter_env.my_own_url); @@ -341,13 +342,20 @@ let main () = 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 batch_update = + try Sys.argv.(1) = "-update" with Invalid_argument _ -> false + in + if batch_update then (* batch mode: performs update and exit *) + Http_getter.update ~logger:Http_getter.stdout_logger () + else begin (* daemon mode: start http daemon *) + 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' *) + end let _ = main ()