X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FproofChecker%2FproofChecker.ml;h=7c9c0f150a1a5068138b3aee594e75a54c88d29a;hb=b5eca1fff4476831847825aa46ce149924d1c8c0;hp=19df81c4ffb29eb5a3ded31d2280004312c8bf3e;hpb=ed6f2ada263b5137d139b45c772fbc010b412f26;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 19df81c4f..7c9c0f150 100644 --- a/helm/proofChecker/proofChecker.ml +++ b/helm/proofChecker/proofChecker.ml @@ -35,7 +35,7 @@ let port = | Failure "int_of_string" -> prerr_endline "Warning: invalid port, reverting to default"; default_port -in +;; let (html_preamble, html_postamble) = ((fun uri -> @@ -53,16 +53,44 @@ let (html_preamble, html_postamble) = END ")) -in +;; let bad_request outchan = printf "INVALID REQUEST !!!!!\n\n"; flush stdout; - Http.Daemon.respond_error ~status:(`Client_error `Bad_request) outchan; + Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan; flush outchan -in +;; + +let usage_string = +" + + + ProofChecker's help message + + +

ProofChecker

Usage

+ Usage: http://hostname:proofcheckerport/command +

+ Available commands: +

+ help
+ display this help message +

+ proofCheck?uri=uri
+ proof-checks the object whose URI is specified by uri +

+ + +" +;; -let callback req outchan = +let callback (req : Http_types.request) outchan = match req#path with | "/proofCheck" -> begin @@ -87,13 +115,14 @@ let callback req outchan = 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; +Http_daemon.start' ~port callback; printf "Proof Checker is terminating, bye!\n" -