aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-01-31 15:57:45 +0100
committerEmilio Jesus Gallego Arias2020-02-24 12:24:40 -0500
commitc216daf5d5f8215947bce10e55d30c35be1a56ba (patch)
treed8b7eaf494bf01ee63d462d54ff85a67359f7c2a /dev/doc
parent46fe9b26ad55a266b71bbd428ee406b03a9db030 (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 'dev/doc')
-rw-r--r--dev/doc/changes.md6
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 42dd2dd052..d5938713d6 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -15,6 +15,12 @@ Exception handling:
`Exninfo.capture` and `iraise` when re-raising inside an exception
handler.
+- Registration of exception printers now follows more closely OCaml's
+ API, thus:
+
+ + printers are of type `exn -> Pp.t option` [`None` == not handled]
+ + it is forbidden for exception printers to raise.
+
Printers:
- Functions such as Printer.pr_lconstr_goal_style_env have been