X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;fp=helm%2FproofChecker%2FproofChecker.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=7c9c0f150a1a5068138b3aee594e75a54c88d29a;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git
diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
deleted file mode 100644
index 7c9c0f150..000000000
--- a/helm/proofChecker/proofChecker.ml
+++ /dev/null
@@ -1,128 +0,0 @@
-(* 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
-"
-
- Proof-Checking %s
-
-
-Proof-Checking %s:
-"
- uri uri)),
-("Done.
-
-
-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 =
-"
-
-
- ProofChecker's help message
-
-
- ProofChecker
- Usage
-
- Usage: http://hostname:proofcheckerport/command
-
-
- Available commands:
-
-
- help
- display this help message
-
-
- proofCheck?uri=uri
- proof-checks the object whose URI is specified by uri
-
-
-
-"
-;;
-
-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"