ocaml 3.09 transition

[helm.git] / helm / proofChecker / proofChecker.ml
diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml

index 5529baa71e06b5ebbb9d73a439009ccd0b6dfabe..e4f00fe3acf86c989b4e250af89000fda4942206 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 ->
@@ -45,10 +37,10 @@ let (html_preamble, html_postamble) =
   <title>Proof-Checking %s</title>
  </head>
  <body bgcolor=\"white\">
-<h1>Proof-Checking %s:</h1>
+<h3>Proof-Checking %s:</h3>
  "
        uri uri)),
-("<h1>Done.</h1>
+("<h3>Done.</h3>
  </body>
  </html>
  END
@@ -58,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
  ;;
  
@@ -90,39 +83,51 @@ 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
-        CicLogger.log_callback :=
-          (CicLogger.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:(`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);
+            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;
+            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;
+CicEnvironment.set_trust (fun _ -> false);
+Http_daemon.start' ~port ~mode:`Fork callback ;
  printf "Proof Checker is terminating, bye!\n"
+