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

diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index 427c75888..3ef0db2e8 100644
--- a/helm/proofChecker/proofChecker.ml
+++ b/helm/proofChecker/proofChecker.ml
@@ -24,21 +24,41 @@
  *)
 
 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 ->
+List of options:"
+ in
+  Arg.parse []
+   (fun _ -> 
+     begin
+      prerr_string "Error: no options expected.\n" ;
+      Arg.usage [] usage_msg ;
+      exit (-1)
+     end
+  ) usage_msg ;
+  try
+   while true do
+    begin
      try
-        CicTypeChecker.typecheck (UriManager.uri_of_string uri)
+      CicTypeChecker.typecheck (UriManager.uri_of_string (read_line ()))
      with
-       e -> print_newline () ; flush stdout ; raise e 
-   ) !uris
+        End_of_file -> raise End_of_file
+      | e ->
+       print_newline() ;
+       flush stdout ;
+       raise e
+    end ;
+    print_endline "END"
+   done
+  with
+   End_of_file -> ()
 ;;
 
+CicCooking.init() ;
+Logger.log_callback :=
+ (Logger.log_to_html
+   ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
 main ();;