-let main () =
- let uris = ref [] in
- Arg.parse []
- (fun uri -> uris := uri :: !uris)
- "
-usage: proofChecker uri ...
-
-List of options:";
- uris := List.rev !uris;
- List.iter
- (function uri ->
- try
- CicTypeChecker.typecheck (UriManager.uri_of_string uri)
- with
- e -> print_newline () ; flush stdout ; raise e
- ) !uris
+open Printf;;
+
+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
+"<html>
+<head>
+ <title>Proof-Checking %s</title>
+</head>
+<body bgcolor=\"white\">
+<h3>Proof-Checking %s:</h3>
+"
+ uri uri)),
+("<h3>Done.</h3>
+</body>
+</html>
+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 =
+"
+<html>
+ <head>
+ <title>ProofChecker's help message</title>
+ </head>
+ <body>
+ <h1>ProofChecker</h1>
+ <h2>Usage</h2>
+ <p>
+ Usage: <kbd>http://hostname:proofcheckerport/</kbd><em>command</em>
+ </p>
+ <p>
+ Available commands:
+ </p>
+ <p>
+ <b><kbd>help</kbd></b><br />
+ display this help message
+ </p>
+ <p>
+ <b><kbd>proofCheck?uri=uri</kbd></b><br />
+ proof-checks the object whose URI is specified by <em>uri</em>
+ </p>
+ </body>
+</html>
+"
+;;
+
+let outchan = ref stderr;;
+
+let _ =
+ HelmLogger.register_log_callback
+ (fun ?append_NL msg ->
+ output_string !outchan (HelmLogger.html_of_html_msg msg) ;
+ flush !outchan)