X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=7c9c0f150a1a5068138b3aee594e75a54c88d29a;hb=0cb00e631ea54deacbfde12e1c458ca602b97870;hp=5467ab43be5590f9b6b8126f2e0d6897aa4edba5;hpb=b216b5a2df4e4218ee2e148cf5e8f11c4d4dbb1b;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 5467ab43b..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; 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; printf "Proof Checker is terminating, bye!\n" -