X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=e4f00fe3acf86c989b4e250af89000fda4942206;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=3ef0db2e8e2e6e9215a753540ff4cfeabf255959;hpb=854ca287626643facb66a9f260f126a8801572c4;p=helm.git
diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index 3ef0db2e8..e4f00fe3a 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,42 +23,111 @@
* 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.
+open Printf;;
-List of options:"
- in
- Arg.parse []
- (fun _ ->
- begin
- prerr_string "Error: no options expected.\n" ;
- Arg.usage [] usage_msg ;
- exit (-1)
- end
- ) usage_msg ;
- 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
- with
- End_of_file -> ()
+let _ = Helm_registry.load_from "/projects/helm/etc/proofChecker.conf.xml";;
+
+let port = Helm_registry.get_int "proofchecker.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 ~code:(`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() ;
-Logger.log_callback :=
- (Logger.log_to_html
- ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
-main ();;
+let outchan = ref stderr;;
+
+let _ =
+ HelmLogger.register_log_callback
+ (fun ?append_NL msg ->
+ output_string !outchan (HelmLogger.html_of_html_msg msg) ;
+ flush !outchan)
+;;
+
+let callback (req : Http_types.request) outchan' =
+ match req#path with
+ | "/proofCheck" ->
+ begin
+ outchan := outchan' ;
+ try
+ let uri = req#param "uri" in
+ 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;
+ flush stdout;
+ fprintf outchan' "%s" (html_preamble uri);
+ flush outchan';
+ (try
+ ignore (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 Http_types.Param_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;
+CicEnvironment.set_trust (fun _ -> false);
+Http_daemon.start' ~port ~mode:`Fork callback ;
+printf "Proof Checker is terminating, bye!\n"
+