diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-14 17:01:16 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-14 17:01:16 +0200 |
| commit | fcdd3fe3c327ecac88880165d14f13ff796510f3 (patch) | |
| tree | cd677c0d8c2c42a19e60365f1678c15a78e82b5c /toplevel | |
| parent | a1eeb3abe387a89cd5a9108160643b6157f9c0af (diff) | |
Allow catching of EvaluatedError exceptions.
We export `Cerrors.EvaluatedError` so plugins and STM consumers can
catch it.
It took me a while to make my mind on this one, but now I am convinced
this is the right thing to do. (Another possibility is to remove
`EvaluatedError` altogether).
The rationale is as follows: when using `Stm.{add,observe}` it
will be frequent for Coq to raise a public-facing exception, however the
toplevel will wrap it into the `EvaluatedError`.
Thus, we get exceptions that we are supposed to handle, but its wrapping
in `EvaluatedError` prevents us from a more meaningful exception
handling: we are stuck with calling the printer.
In particular, this allows SerAPI/jsCoq to provide proper serialization
of most public exceptions.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index a0e3e3c19..cd6ccd565 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Toplevel Exception *) +exception EvaluatedError of Pp.std_ppcmds * exn option + (** Error report. *) val print_loc : Loc.t -> Pp.std_ppcmds |