diff options
author | 2016-12-27 16:53:30 +0100 | |
---|---|---|
committer | 2016-12-27 18:33:25 +0100 | |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /lib/errors.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'lib/errors.ml')
-rw-r--r-- | lib/errors.ml | 141 |
1 files changed, 0 insertions, 141 deletions
diff --git a/lib/errors.ml b/lib/errors.ml deleted file mode 100644 index c1d224df..00000000 --- a/lib/errors.ml +++ /dev/null @@ -1,141 +0,0 @@ -(***********************************************************************) -(* 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 *) -(***********************************************************************) - -open Pp - -(** Aliases *) - -let push = Backtrace.add_backtrace - -(* Errors *) - -exception Anomaly of string option * std_ppcmds (* System errors *) - -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 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)) - -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) - -exception Timeout -exception Drop -exception Quit - -let handle_stack = ref [] - -exception Unhandled - -let register_handler h = handle_stack := h::!handle_stack - -(** [print_gen] is a general exception printer which tries successively - all the handlers of a list, and finally a [bottom] handler if all - others have failed *) - -let rec print_gen bottom stk e = - match stk with - | [] -> bottom e - | h::stk' -> - try h e - with - | Unhandled -> print_gen bottom stk' e - | any -> print_gen bottom stk' any - -(** Only anomalies should reach the bottom of the handler stack. - In usual situation, the [handle_stack] is treated as it if was always - non-empty with [print_anomaly] as its bottom handler. *) - -let where = function -| None -> mt () -| Some s -> - 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 "." - | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "." - | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." - -let print_backtrace e = match Backtrace.get_backtrace e with -| None -> mt () -| Some bt -> - let bt = Backtrace.repr bt in - let pr_frame f = str (Backtrace.print_frame f) in - let bt = prlist_with_sep fnl pr_frame bt in - fnl () ++ hov 0 bt - -let print_anomaly askreport e = - if askreport then - hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.") - else - hov 0 (raw_anomaly e) - -(** The standard exception printer *) -let print ?(info = Exninfo.null) e = - print_gen (print_anomaly true) !handle_stack e ++ print_backtrace info - -let iprint (e, info) = print ~info e - -(** Same as [print], except that the "Please report" part of an anomaly - isn't printed (used in Ltac debugging). *) -let print_no_report e = print_gen (print_anomaly false) !handle_stack e -let iprint_no_report (e, info) = - print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info - -(** Predefined handlers **) - -let _ = register_handler begin function - | UserError(s, pps) -> - hov 0 (str "Error: " ++ where (Some s) ++ pps) - | _ -> raise Unhandled -end - -(** Critical exceptions should not be caught and ignored by mistake - by inner functions during a [vernacinterp]. They should be handled - only at the very end of interp, to be displayed to the user. *) - -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 - -(** Check whether an exception is handled *) - -exception Bottom - -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; - flush_all (); - exit (if anomaly then 129 else 1) |