From: Claudio Sacerdoti Coen Date: Mon, 23 Jun 2003 14:31:45 +0000 (+0000) Subject: - help method added X-Git-Tag: V7_3_new_exportation_merged~3 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=37adb260bc671a4615e2b3fa9fb1ae44999747d0 - help method added - branch V7_3_new_exportation merged --- 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" -