X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FproofChecker%2FproofChecker.ml;h=7c9c0f150a1a5068138b3aee594e75a54c88d29a;hb=4faf0e37e7019de16dd6862bb34d84f799a2a230;hp=4dfcb70b303af82d07f6d454776695ef47c16afd;hpb=865edc29497caf418f9cc60d982d2bfc6c02880e;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 4dfcb70b3..7c9c0f150 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,106 @@ * 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 +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 +" +
++ 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
+