X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=7c9c0f150a1a5068138b3aee594e75a54c88d29a;hb=789a37bedf2a8ce2a0b4389fb5c48a0a7b6572d6;hp=3ef0db2e8e2e6e9215a753540ff4cfeabf255959;hpb=854ca287626643facb66a9f260f126a8801572c4;p=helm.git diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml index 3ef0db2e8..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,42 +23,106 @@ * http://cs.unibo.it/helm/. *) -let main () = - let usage_msg = - " -usage: proofChecker[.opt] -The proof-checker reads from the stdin one URI at a time and proof-checks it. +open Printf;; -List of options:" - in - Arg.parse [] - (fun _ -> - begin - prerr_string "Error: no options expected.\n" ; - Arg.usage [] usage_msg ; - exit (-1) - end - ) usage_msg ; +let default_port = 48084;; + +let port = try - while true do - begin - try - CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ())) - with - End_of_file -> raise End_of_file - | e -> - print_newline() ; - flush stdout ; - raise e - end ; - print_endline "END" - done + int_of_string (Sys.getenv "PROOF_CHECKER_PORT") with - End_of_file -> () + | 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
+