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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
(***********************************************************************)
(* 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
(* Errors *)
type backtrace = string option
exception Anomaly of string option * std_ppcmds * backtrace (* System errors *)
let get_backtrace () =
if !Flags.debug then Some (Printexc.get_backtrace ())
else None
let make_anomaly ?label pp =
let bt = get_backtrace () in
Anomaly (label, pp, bt)
let anomaly_gen label pp =
let bt = get_backtrace () in
raise (Anomaly (label, pp, bt))
let anomaly ?loc ?label pp =
let bt = get_backtrace () in
match loc with
| None -> raise (Anomaly (label, pp, bt))
| Some loc ->
Loc.raise loc (Anomaly (label, pp, bt))
let anomalylabstrm string pps =
anomaly_gen (Some string) pps
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)
(* Like Exc_located, but specifies the outermost file read, the filename
associated to the location of the error, and the error itself. *)
exception Error_in_file of string * (bool * string * Loc.t) * exn
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
| e' -> print_gen bottom stk' e'
(** 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 "^s^":") ++ spc () else mt ()
let raw_anomaly e = match e with
| Anomaly (s, pps, bt) -> where s ++ pps ++ str "."
| Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
| _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
let print_anomaly askreport e =
let bt_info = match e with
| Anomaly (_, _, Some bt) -> (fnl () ++ hov 0 (str bt))
| _ -> mt ()
in
let info =
if askreport then
hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
else
hov 0 (raw_anomaly e)
in
info ++ bt_info
(** The standard exception printer *)
let print e = print_gen (print_anomaly true) !handle_stack 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 print_anomaly e = print_anomaly true e
(** Same as [print], except that anomalies are not printed but re-raised
(used for the Fail command) *)
let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
(** Predefined handlers **)
let _ = register_handler begin function
| UserError(s,pps) -> hov 0 (str "Error: " ++ where (Some s) ++ pps)
| _ -> raise Unhandled
end
|
