From f0341076aa60a84177a6b46db0d8d50df220536b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 6 Dec 2016 17:16:16 +0100 Subject: [error] Move back fatal_error to toplevel This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09 (the mllib dependencies that should be surely tweaked more). The logic for `fatal_error` has no place in `CErrors`, this is coqtop-specific code. What is more, a libobject caller should handle the exception correctly, I fail to see why the fix was needed on the first place. --- lib/cErrors.ml | 10 ---------- lib/cErrors.mli | 5 ----- library/libobject.ml | 12 ++---------- toplevel/coqtop.ml | 7 +++++++ 4 files changed, 9 insertions(+), 25 deletions(-) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 9cbc3fb6d..a05964039 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -147,13 +147,3 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false - -(** Prints info which is either an error or - an anomaly and then exits with the appropriate - error code *) - -let fatal_error info anomaly = - let msg = info ++ fnl () in - pp_with !Pp_control.err_ft msg; - Format.pp_print_flush !Pp_control.err_ft (); - exit (if anomaly then 129 else 1) diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 5cffc725d..0665a8ce7 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -98,8 +98,3 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool - -(** Prints info which is either an error or - an anomaly and then exits with the appropriate - error code *) -val fatal_error : Pp.std_ppcmds -> bool -> 'a diff --git a/library/libobject.ml b/library/libobject.ml index caa03c85b..8757ca08c 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -91,16 +91,8 @@ let declare_object_full odecl = dyn_rebuild_function = rebuild }; (infun,outfun) -(* The "try .. with .. " allows for correct printing when calling - declare_object a loading time. -*) - -let declare_object odecl = - try fst (declare_object_full odecl) - with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) -let declare_object_full odecl = - try declare_object_full odecl - with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) +let declare_object odecl = fst (declare_object_full odecl) +let declare_object_full odecl = declare_object_full odecl (* this function describes how the cache, load, open, and export functions are triggered. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0ece0b014..541c1fd1b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -431,6 +431,13 @@ let get_native_name s = Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" +(** Prints info which is either an error or an anomaly and then exits + with the appropriate error code *) +let fatal_error info anomaly = + let msg = info ++ fnl () in + Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg; + exit (if anomaly then 129 else 1) + let parse_args arglist = let args = ref arglist in let extras = ref [] in -- cgit v1.2.3