| Failure "int_of_string" ->
prerr_endline "Warning: invalid port, reverting to default";
default_port
-in
+;;
let (html_preamble, html_postamble) =
((fun uri ->
</html>
END
"))
-in
+;;
let bad_request outchan =
printf "INVALID REQUEST !!!!!\n\n";
flush stdout;
Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
flush outchan
-in
+;;
+
+let usage_string =
+"
+<html>
+ <head>
+ <title>ProofChecker's help message</title>
+ </head>
+ <body>
+ <h1>ProofChecker</h1>
+ <h2>Usage</h2>
+ <p>
+ Usage: <kbd>http://hostname:proofcheckerport/</kbd><em>command</em>
+ </p>
+ <p>
+ Available commands:
+ </p>
+ <p>
+ <b><kbd>help</kbd></b><br />
+ display this help message
+ </p>
+ <p>
+ <b><kbd>proofCheck?uri=uri</kbd></b><br />
+ proof-checks the object whose URI is specified by <em>uri</em>
+ </p>
+ </body>
+</html>
+"
+;;
-let callback req outchan =
+let callback (req : Http_types.request) outchan =
match req#path with
| "/proofCheck" ->
begin
with Not_found -> (* 'uri' argument not found *)
bad_request outchan
end
+ | "/help" ->
+ Http_daemon.respond ~body:usage_string
+ ~headers:["Content-Type", "text/html"] outchan
| req -> bad_request outchan
in
-CicCooking.init();
printf "Proof Checker started and listening on port %d\n" port;
flush stdout;
Http_daemon.start' ~port callback;
printf "Proof Checker is terminating, bye!\n"
-
projects / helm.git / commitdiff