1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** 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 -> Pp.t -> exn
(** Create an anomaly. *)
val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> '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 option * Pp.t
(** Main error signaling exception. It carries a header plus a pretty printing
doc *)
val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a
(** Main error raising primitive. [user_err ?loc ?hdr pp] signals an
error [pp] with optional header and location [hdr] [loc] *)
exception AlreadyDeclared of Pp.t
val alreadydeclared : Pp.t -> '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
(** [register_handler h] registers [h] as a handler.
When an expression is printed with [print e], it
goes through all registered handles (the most
recent first) until a handle deals with it.
Handles signal that they don't deal with some exception
by raising [Unhandled].
Handles can raise exceptions themselves, in which
case, the exception is passed to the handles which
were registered before.
The exception that are considered anomalies should not be
handled by registered handlers.
*)
exception Unhandled
val register_handler : (exn -> Pp.t) -> unit
(** The standard exception printer *)
val print : ?info:Exninfo.info -> exn -> Pp.t
val iprint : Exninfo.iexn -> Pp.t
(** 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.t
val iprint_no_report : Exninfo.iexn -> Pp.t
(** Critical exceptions should not be caught 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], [Assert_failure], [Anomaly] ...
*)
val noncritical : exn -> bool
(** Check whether an exception is handled by some toplevel printer. The
[Anomaly] exception is never handled. *)
val handled : exn -> bool
|
