X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FproofChecker%2FproofChecker.ml;h=81ef46c7f8b251aba50aaf8aec8ced51c7177a29;hb=edeecdcf2cb51318a7d4c608652f4f988e80f66f;hp=427c75888cd7ee07266529dd3624b0e28a885d1a;hpb=fccd7efbf01edf574b0f2c40994793b80648179d;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 427c75888..81ef46c7f 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,22 +23,76 @@ * 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 -;; - -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 +" +
+