diff options
| author | Emilio Jesus Gallego Arias | 2020-01-31 15:57:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-24 12:24:40 -0500 |
| commit | c216daf5d5f8215947bce10e55d30c35be1a56ba (patch) | |
| tree | d8b7eaf494bf01ee63d462d54ff85a67359f7c2a /lib/cErrors.mli | |
| parent | 46fe9b26ad55a266b71bbd428ee406b03a9db030 (diff) | |
[exn] Forbid raising in exn printers, make them return Pp.t option
Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.
We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
Diffstat (limited to 'lib/cErrors.mli')
| -rw-r--r-- | lib/cErrors.mli | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 02eaf6bd0b..1660a00244 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -46,19 +46,14 @@ exception Timeout recent first) until a handle deals with it. Handles signal that they don't deal with some exception - by raising [Unhandled]. + by returning None. Raising any other exception is + forbidden and will result in an anomaly. - 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 + Exceptions that are considered anomalies should not be handled by registered handlers. *) -exception Unhandled - -val register_handler : (exn -> Pp.t) -> unit +val register_handler : (exn -> Pp.t option) -> unit (** The standard exception printer *) val print : exn -> Pp.t |