From cc5d102f0d9e3eef2e7b810c47002f26335601db Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 17 May 2011 17:02:59 +0000
Subject: More work on error handling

 Anomalies are now meant to be the exceptions that are *not*
 catched and handled by the new Errors.handle_stack.

 Three variants of [Errors.print] allow to customize how anomalies
 are treated. In particular, [Errors.print_no_anomaly] is used
 for the Fail command, instead of a classification function
 Cerrors.is_user_error which wasn't customizable.

 No more AnomalyOnError, its only occurrence is now a regular anomaly

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14133 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/errors.mli | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'lib/errors.mli')

diff --git a/lib/errors.mli b/lib/errors.mli
index 120634e60d..eb7fde8e77 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -15,13 +15,27 @@
     recent first) until a handle deals with it.
 
     Handles signal that they don't deal with some exception
-    by raisine [Unhandled].
+    by raising [Unhandled].
 
     Handles can raise exceptions themselves, in which
     case, the exception is passed to the handles which
-    were registered before. *)
+    were registered before.
+
+    The exception that are considered anomalies should not be
+    handled by registered handlers.
+*)
+
 exception Unhandled
 
 val register_handler : (exn -> Pp.std_ppcmds) -> unit
 
+(** The standard exception printer *)
 val print : exn -> Pp.std_ppcmds
+
+(** Same as [print], except that the "Please report" part of an anomaly
+    isn't printed (used in Ltac debugging). *)
+val print_no_report : exn -> Pp.std_ppcmds
+
+(** Same as [print], except that anomalies are not printed but re-raised
+    (used for the Fail command) *)
+val print_no_anomaly : exn -> Pp.std_ppcmds
-- 
cgit v1.2.3