+++ /dev/null
-(* Copyright (C) 2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-open Printf;;
-
-let default_port = 48084;;
-
-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 (html_preamble, html_postamble) =
- ((fun uri ->
- (sprintf
-"<html>
-<head>
- <title>Proof-Checking %s</title>
-</head>
-<body bgcolor=\"white\">
-<h1>Proof-Checking %s:</h1>
-"
- uri uri)),
-("<h1>Done.</h1>
-</body>
-</html>
-END
-"))
-;;
-
-let bad_request outchan =
- printf "INVALID REQUEST !!!!!\n\n";
- flush stdout;
- Http_daemon.respond_error ~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 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));
- 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
- | "/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;
-Http_daemon.start' ~port callback;
-printf "Proof Checker is terminating, bye!\n"
projects / helm.git / blobdiff