diff options
| author | Pierre-Marie Pédrot | 2020-05-16 13:57:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-16 13:57:58 +0200 |
| commit | ebaaa7371c3a3548ccec1836621726f6d829858a (patch) | |
| tree | f5bfbfa5ad485e7c2f7b680de794b2005506bef9 /lib | |
| parent | 2111994285a21df662c232fa5acfd60e8a640795 (diff) | |
| parent | 8fd01b538c5b4ea58eecf8be07ab8115619cca4d (diff) | |
Merge PR #11566: [misc] Better preserve backtraces in several modules
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 11 | ||||
| -rw-r--r-- | lib/cErrors.mli | 4 |
2 files changed, 10 insertions, 5 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 62d465c703..cb64e36755 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -25,12 +25,17 @@ let _ = in Printexc.register_printer pr -let anomaly ?loc ?label pp = - Loc.raise ?loc (Anomaly (label, pp)) +let anomaly ?loc ?info ?label pp = + let info = Option.default Exninfo.null info in + let info = Option.cata (Loc.add_loc info) info loc in + Exninfo.iraise (Anomaly (label, pp), info) exception UserError of string option * Pp.t (* User errors *) -let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) +let user_err ?loc ?info ?hdr strm = + let info = Option.default Exninfo.null info in + let info = Option.cata (Loc.add_loc info) info loc in + Exninfo.iraise (UserError (hdr, strm), info) exception Timeout diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 21d41c996d..cf1857cf04 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -21,7 +21,7 @@ val push : exn -> Exninfo.iexn [Anomaly] is used for system errors and [UserError] for the user's ones. *) -val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a +val anomaly : ?loc:Loc.t -> ?info:Exninfo.info -> ?label:string -> Pp.t -> 'a (** Raise an anomaly, with an optional location and an optional label identifying the anomaly. *) @@ -34,7 +34,7 @@ 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 +val user_err : ?loc:Loc.t -> ?info:Exninfo.info -> ?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] *) |
