diff options
Diffstat (limited to 'driver/Driveraux.ml')
-rw-r--r-- | driver/Driveraux.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 6d8d0adc..ccc3d00d 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -13,6 +13,7 @@ open Printf open Clflags +open Diagnostics (* Safe removal of files *) let safe_remove file = @@ -46,9 +47,9 @@ let command stdout args = match status with | Unix.WEXITED rc -> rc | Unix.WSIGNALED n | Unix.WSTOPPED n -> - eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 + error no_loc "Command '%s' killed on a signal." argv.(0); -1 with Unix.Unix_error(err, fn, param) -> - eprintf "Error executing '%s': %s: %s %s\n" + error no_loc "executing '%s': %s: %s %s" argv.(0) fn (Unix.error_message err) param; -1 @@ -81,7 +82,7 @@ let command ?stdout args = command stdout args let command_error n exc = - eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc + fatal_error no_loc "%s command failed with exit code %d (use -v to see invocation)\n" n exc (* Determine names for output files. We use -o option if specified @@ -105,20 +106,18 @@ let output_filename_default default_file = (* All input files should exist *) let ensure_inputfile_exists name = - if not (Sys.file_exists name) then begin - eprintf "error: no such file or directory: '%s'\n" name; - exit 2 - end + if not (Sys.file_exists name) then + fatal_error no_loc "no such file or directory: '%s'" name + (* Printing of error messages *) -let print_error oc msg = +let print_error pp msg = let print_one_error = function - | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s) - | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i) - | Errors.POS i -> fprintf oc "%ld" (Camlcoq.P.to_int32 i) + | Errors.MSG s -> Format.pp_print_string pp (Camlcoq.camlstring_of_coqstring s) + | Errors.CTX i -> Format.pp_print_string pp (Camlcoq.extern_atom i) + | Errors.POS i -> Format.fprintf pp "%ld" (Camlcoq.P.to_int32 i) in - List.iter print_one_error msg; - output_char oc '\n' + List.iter print_one_error msg (* Command-line parsing *) let explode_comma_option s = |