From fcdd3fe3c327ecac88880165d14f13ff796510f3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Jun 2016 17:01:16 +0200 Subject: 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. --- toplevel/cerrors.mli | 3 +++ 1 file changed, 3 insertions(+) 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 -- cgit v1.2.3