+++ /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 _ = 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)
-;;
-
-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"
-