...

[helm.git] / helm / proofChecker / proofChecker.ml

diff --git a/helm/proofChecker/proofChecker.ml b/helm/proofChecker/proofChecker.ml
index 4dfcb70b303af82d07f6d454776695ef47c16afd..3ef0db2e8e2e6e9215a753540ff4cfeabf255959 100644 (file)
--- a/helm/proofChecker/proofChecker.ml
+++ b/helm/proofChecker/proofChecker.ml
@@ -24,22 +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 ();;