blob: ae4d0b852bc3884b9c1c1d7f206dc1ee28c3bcab (
plain)
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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(** This modules implements basic manipulations of errors for use
throughout Coq's code. *)
(** [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.std_ppcmds) -> unit
(** The standard exception printer *)
val print : exn -> 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...
*)
val noncritical : exn -> bool
|
