Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 25 insertions, 44 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 5c56192f..97502211 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -1,10 +1,12 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
 
 open Pp
 
@@ -14,17 +16,7 @@ let push = Backtrace.add_backtrace
 
 (* Errors *)
 
-exception Anomaly of string option * std_ppcmds (* System errors *)
-
-(* XXX: To move to common tagging functions in Pp, blocked on tag
- * system cleanup as we cannot define generic error tags now.
- *
- * Anyways, tagging should not happen here, but in the specific
- * listener to the msg_* stuff.
- *)
-let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
-let err_str       = tag_err_str "Error:"
-let ann_str       = tag_err_str "Anomaly:"
+exception Anomaly of string option * Pp.t (* System errors *)
 
 let _ =
   let pr = function
@@ -36,25 +28,23 @@ let _ =
 let make_anomaly ?label pp =
   Anomaly (label, pp)
 
-let anomaly ?loc ?label pp = match loc with
-  | None -> raise (Anomaly (label, pp))
-  | Some loc -> Loc.raise loc (Anomaly (label, pp))
+let anomaly ?loc ?label pp =
+  Loc.raise ?loc (Anomaly (label, pp))
 
 let is_anomaly = function
 | Anomaly _ -> true
 | _ -> false
 
-exception UserError of string * std_ppcmds (* User errors *)
-let error string = raise (UserError("_", str string))
-let errorlabstrm l pps = raise (UserError(l,pps))
-
-exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
-let alreadydeclared pps = raise (AlreadyDeclared(pps))
+exception UserError of string option * Pp.t (* User errors *)
 
 let todo s = prerr_string ("TODO: "^s^"\n")
 
-let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
-let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
+let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm))
+
+let invalid_arg ?loc s   = Loc.raise ?loc (Invalid_argument s)
+
+exception AlreadyDeclared of Pp.t (* for already declared Schemes *)
+let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
 exception Timeout
 exception Drop
@@ -89,7 +79,7 @@ let where = function
   if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt ()
 
 let raw_anomaly e = match e with
-  | Anomaly (s, pps) -> where s ++ pps ++ str "."
+  | Anomaly (s, pps) -> where s ++ pps
   | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "."
   | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
 
@@ -103,9 +93,8 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (ann_str ++ raw_anomaly e ++ spc () ++
-           strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
-           str ".")
+    hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++
+    hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")
   else
     hov 0 (raw_anomaly e)
 
@@ -125,7 +114,7 @@ let iprint_no_report (e, info) =
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    hov 0 (err_str ++ where (Some s) ++ pps)
+    hov 0 (where s ++ pps)
   | _ -> raise Unhandled
 end
 
@@ -133,12 +122,14 @@ end
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user. *)
 
+[@@@ocaml.warning "-52"]
 let noncritical = function
   | Sys.Break | Out_of_memory | Stack_overflow
   | Assert_failure _ | Match_failure _ | Anomaly _
   | Timeout | Drop | Quit -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
+[@@@ocaml.warning "+52"]
 
 (** Check whether an exception is handled *)
 
@@ -148,13 +139,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_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
-  Format.pp_print_flush !Pp_control.err_ft ();
-  exit (if anomaly then 129 else 1)