X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FproofChecker%2FproofChecker.ml;h=1c7245164147eb8227b4ffb1c86418a6a13cf867;hb=f6e4a271838bc59f3b22e68a282dc995776360cb;hp=427c75888cd7ee07266529dd3624b0e28a885d1a;hpb=fccd7efbf01edf574b0f2c40994793b80648179d;p=helm.git

diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index 427c75888..1c7245164 100644
--- a/helm/proofChecker/proofChecker.ml
+++ b/helm/proofChecker/proofChecker.ml
@@ -24,21 +24,34 @@
  *)
 
 let main () =
- let uris = ref [] in
- Arg.parse []
-  (fun uri -> uris :=  uri :: !uris)
+ let usage_msg =
   "
-usage: proofChecker uri ...
+usage: proofChecker[.opt]
+The proof-checker reads from the stdin one URI at a time and proof-checks it.
 
-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
+List of options:"
+ in
+  Arg.parse []
+   (fun _ -> 
+     begin
+      prerr_string "Error: no options expected.\n" ;
+      Arg.usage [] usage_msg ;
+      exit (-1)
+     end
+  ) usage_msg ;
+  while true do
+   begin
+    try
+     CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ()))
+    with
+     e ->
+      print_newline() ;
+      flush stdout ;
+      raise e
+   end ;
+   print_endline "END"
+  done
 ;;
 
+CicCooking.init() ;
 main ();;