X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=7c9c0f150a1a5068138b3aee594e75a54c88d29a;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=1c7245164147eb8227b4ffb1c86418a6a13cf867;hpb=84e62facde0ee126b5f08dd376086acd861a9320;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 1c7245164..7c9c0f150 100644 --- a/helm/proofChecker/proofChecker.ml +++ b/helm/proofChecker/proofChecker.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,35 +23,106 @@ * http://cs.unibo.it/helm/. *) -let main () = - let usage_msg = - " -usage: proofChecker[.opt] -The proof-checker reads from the stdin one URI at a time and proof-checks it. - -List of options:" - in - Arg.parse [] - (fun _ -> - begin - prerr_string "Error: no options expected.\n" ; - Arg.usage [] usage_msg ; - exit (-1) - end - ) usage_msg ; - while true do - begin - try - CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ())) - with - e -> - print_newline() ; - flush stdout ; - raise e - end ; - print_endline "END" - done +open Printf;; + +let default_port = 48084;; + +let port = + try + int_of_string (Sys.getenv "PROOF_CHECKER_PORT") + with + | Not_found -> default_port + | Failure "int_of_string" -> + prerr_endline "Warning: invalid port, reverting to default"; + default_port +;; + +let (html_preamble, html_postamble) = + ((fun uri -> + (sprintf +" + + Proof-Checking %s + + +

Proof-Checking %s:

+" + uri uri)), +("

Done.

+ + +END +")) +;; + +let bad_request outchan = + printf "INVALID REQUEST !!!!!\n\n"; + flush stdout; + Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan; + flush outchan +;; + +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 +

+ + +" ;; -CicCooking.init() ; -main ();; +let callback (req : Http_types.request) outchan = + match req#path with + | "/proofCheck" -> + begin + Logger.log_callback := + (Logger.log_to_html + ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan)); + try + let uri = req#param "uri" in + printf "Request to proof-check \"%s\"..." uri; + flush stdout; + fprintf outchan "%s" (html_preamble uri); + flush outchan; + (try + CicTypeChecker.typecheck (UriManager.uri_of_string uri); + with e -> + fprintf outchan "%s\n" (Printexc.to_string e); + flush outchan); + fprintf outchan "%s" html_postamble; + flush outchan; + printf " done\n\n"; + flush stdout + 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 + +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"