X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=5467ab43be5590f9b6b8126f2e0d6897aa4edba5;hb=a4df9661e15509e5da6ed9c57e3ab6a27a440c3f;hp=4dfcb70b303af82d07f6d454776695ef47c16afd;hpb=865edc29497caf418f9cc60d982d2bfc6c02880e;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 4dfcb70b3..5467ab43b 100644 --- a/helm/proofChecker/proofChecker.ml +++ b/helm/proofChecker/proofChecker.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,23 +23,77 @@ * http://cs.unibo.it/helm/. *) -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 -;; - -CicCooking.init() ; -main ();; +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 +in + +let (html_preamble, html_postamble) = + ((fun uri -> + (sprintf +" +
+