aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driveraux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Driveraux.ml')
-rw-r--r--driver/Driveraux.ml25
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 =