*)
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 ();;