X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=5467ab43be5590f9b6b8126f2e0d6897aa4edba5;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=d7cf692849933d6a51fb0ac07b1b73ee882f0129;hpb=daa3373748a896d0b5fc00c0d6b79f59e79a128d;p=helm.git
diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index d7cf69284..5467ab43b 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,39 +23,77 @@
* 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 ;
+open Printf;;
+
+let default_port = 48084;;
+
+let port =
try
- while true do
- begin
- try
- CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ()))
- with
- End_of_file -> raise End_of_file
- | e ->
- print_newline() ;
- flush stdout ;
- raise e
- end ;
- print_endline "END"
- done
+ int_of_string (Sys.getenv "PROOF_CHECKER_PORT")
with
- End_of_file -> ()
-;;
+ | Not_found -> default_port
+ | Failure "int_of_string" ->
+ prerr_endline "Warning: invalid port, reverting to default";
+ default_port
+in
+
+let (html_preamble, html_postamble) =
+ ((fun uri ->
+ (sprintf
+"
+
+ Proof-Checking %s
+
+
+Proof-Checking %s:
+"
+ uri uri)),
+("Done.
+
+
+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 callback req 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
+ | 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"
-CicCooking.init() ;
-main ();;