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