X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=e4f00fe3acf86c989b4e250af89000fda4942206;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=13704366084762d0a26750cd4db1a8a90d118b9f;hpb=6f0f31787fb03ea4956227e8fcdbc12abd366931;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 137043660..e4f00fe3a 100644 --- a/helm/proofChecker/proofChecker.ml +++ b/helm/proofChecker/proofChecker.ml @@ -25,14 +25,9 @@ open Printf;; -let _ = Helm_registry.load_from "proofChecker.conf.xml";; +let _ = Helm_registry.load_from "/projects/helm/etc/proofChecker.conf.xml";; -let port = - try - Helm_registry.get_int "proofchecker.port" - with - Helm_registry.Key_not_found _ -> 48084 -;; +let port = Helm_registry.get_int "proofchecker.port";; let (html_preamble, html_postamble) = ((fun uri -> @@ -42,10 +37,10 @@ let (html_preamble, html_postamble) = Proof-Checking %s -

Proof-Checking %s:

+

Proof-Checking %s:

" uri uri)), -("

Done.

+("

Done.

END @@ -55,7 +50,8 @@ END 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 ~code:(`Status (`Client_error `Bad_request)) + outchan; flush outchan ;; @@ -103,7 +99,7 @@ let callback (req : Http_types.request) outchan' = outchan := outchan' ; try let uri = req#param "uri" in - Http_daemon.send_basic_headers ~code:200 outchan' ; + Http_daemon.send_basic_headers ~code:(`Code 200) outchan' ; Http_daemon.send_header "Content-type" "text/html" outchan' ; Http_daemon.send_CRLF outchan' ; printf "Request to proof-check \"%s\"..." uri; @@ -111,7 +107,7 @@ let callback (req : Http_types.request) outchan' = fprintf outchan' "%s" (html_preamble uri); flush outchan'; (try - CicTypeChecker.typecheck (UriManager.uri_of_string uri); + ignore (CicTypeChecker.typecheck (UriManager.uri_of_string uri)); with e -> fprintf outchan' "%s\n" (Printexc.to_string e); flush outchan'); @@ -131,5 +127,7 @@ in printf "Proof Checker started and listening on port %d\n" port; flush stdout; +CicEnvironment.set_trust (fun _ -> false); Http_daemon.start' ~port ~mode:`Fork callback ; printf "Proof Checker is terminating, bye!\n" +