X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=5467ab43be5590f9b6b8126f2e0d6897aa4edba5;hb=28094cb186c862ac29f95e32f146ebaa59becb5a;hp=427c75888cd7ee07266529dd3624b0e28a885d1a;hpb=fccd7efbf01edf574b0f2c40994793b80648179d;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 427c75888..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,22 +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 -;; - -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 +" +
+