first moogle template checkin

[helm.git] / helm / proofChecker / proofChecker.ml

diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index 7c9c0f150a1a5068138b3aee594e75a54c88d29a..6513d4f930085eb020258a8e01117575357c44df 100644 (file)
--- a/helm/proofChecker/proofChecker.ml
+++ b/helm/proofChecker/proofChecker.ml
@@ -25,17 +25,9 @@
 
 open Printf;;
 
-let default_port = 48084;;
+let _ = Helm_registry.load_from "/projects/helm/etc/proofChecker.conf.xml";;
 
-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 port = Helm_registry.get_int "proofchecker.port";;
 
 let (html_preamble, html_postamble) =
   ((fun uri ->
@@ -90,39 +82,49 @@ let usage_string =
 "
 ;;
 
-let callback (req : Http_types.request) outchan =
+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
-        Logger.log_callback :=
-          (Logger.log_to_html
-            ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan));
+        outchan := outchan' ;
         try
           let uri = req#param "uri" in
+          Http_daemon.send_basic_headers ~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;
+          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;
+            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
+        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
+       ~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;
+Http_daemon.start' ~port ~mode:`Fork callback ;
 printf "Proof Checker is terminating, bye!\n"