diff options
Diffstat (limited to 'lib/errors.mli')
| -rw-r--r-- | lib/errors.mli | 54 |
1 files changed, 47 insertions, 7 deletions
diff --git a/lib/errors.mli b/lib/errors.mli index ae4d0b85..e4096a7e 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -6,9 +6,53 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +open Pp + (** This modules implements basic manipulations of errors for use throughout Coq's code. *) +(** {6 Error handling} *) + +val push : exn -> Exninfo.iexn +(** Alias for [Backtrace.add_backtrace]. *) + +(** {6 Generic errors.} + + [Anomaly] is used for system errors and [UserError] for the + user's ones. *) + +val make_anomaly : ?label:string -> std_ppcmds -> exn +(** Create an anomaly. *) + +val anomaly : ?loc:Loc.t -> ?label:string -> std_ppcmds -> 'a +(** Raise an anomaly, with an optional location and an optional + label identifying the anomaly. *) + +val is_anomaly : exn -> bool +(** Check whether a given exception is an anomaly. + This is mostly provided for compatibility. Please avoid doing specific + tricks with anomalies thanks to it. See rather [noncritical] below. *) + +exception UserError of string * std_ppcmds +val error : string -> 'a +val errorlabstrm : string -> std_ppcmds -> 'a +val user_err_loc : Loc.t * string * std_ppcmds -> 'a + +exception AlreadyDeclared of std_ppcmds +val alreadydeclared : std_ppcmds -> 'a + +val invalid_arg_loc : Loc.t * string -> 'a + +(** [todo] is for running of an incomplete code its implementation is + "do nothing" (or print a message), but this function should not be + used in a released code *) + +val todo : string -> unit + +exception Timeout +exception Drop +exception Quit + (** [register_handler h] registers [h] as a handler. When an expression is printed with [print e], it goes through all registered handles (the most @@ -30,20 +74,16 @@ exception Unhandled val register_handler : (exn -> Pp.std_ppcmds) -> unit (** The standard exception printer *) -val print : exn -> Pp.std_ppcmds +val print : ?info:Exninfo.info -> exn -> Pp.std_ppcmds +val iprint : Exninfo.iexn -> Pp.std_ppcmds (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) val print_no_report : exn -> Pp.std_ppcmds -(** Same as [print], except that anomalies are not printed but re-raised - (used for the Fail command) *) -val print_no_anomaly : exn -> Pp.std_ppcmds - (** Critical exceptions shouldn't be catched and ignored by mistake by inner functions during a [vernacinterp]. They should be handled only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user. - Typical example: [Sys.Break]. In the 8.4 branch, for maximal - compatibility, anomalies are not considered as critical... + Typical example: [Sys.Break], [Assert_failure], [Anomaly] ... *) val noncritical : exn -> bool |