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

4 files changed, 54 insertions, 32 deletions

diff --git a/lib/errors.ml b/lib/errors.ml
index 89e924948e..3b5e67704a 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -10,7 +10,6 @@ open Pp
 
 (* spiwack: it might be reasonable to decide and move the declarations
    of Anomaly and so on to this module so as not to depend on Util. *)
-(* spiwack: This module contains stuff exfiltrated from Cerrors. *)
 
 let handle_stack = ref []
 
@@ -18,39 +17,52 @@ exception Unhandled
 
 let register_handler h = handle_stack := h::!handle_stack
 
-(* spiwack: [anomaly_string] and [report_fn] are copies from Cerrors.
-   Ultimately they should disapear from Cerrors. *)
-let anomaly_string () = str "Anomaly: "
-let report_fn () = (str "." ++ spc () ++ str "Please report.")
-(* [print_unhandled_exception] is the virtual bottom of the stack:
-   the [handle_stack] is treated as it if was always non-empty
-   with [print_unhandled_exception] as its last handler. *)
-let print_unhandled_exception e =
-  hov 0 (anomaly_string () ++ str "Uncaught exception " ++
-	 str (Printexc.to_string e) ++ report_fn ())
-
-let rec print_gen s e =
-  match s with
-  | [] -> print_unhandled_exception e
-  | h::s' ->
+(** [print_gen] is a general exception printer which tries successively
+    all the handlers of a list, and finally a [bottom] handler if all
+    others have failed *)
+
+let rec print_gen bottom stk e =
+  match stk with
+  | [] -> bottom e
+  | h::stk' ->
     try h e
     with
-    | Unhandled -> print_gen s' e
-    | e' -> print_gen s' e'
+    | Unhandled -> print_gen bottom stk' e
+    | e' -> print_gen bottom stk' e'
+
+(** Only anomalies should reach the bottom of the handler stack.
+    In usual situation, the [handle_stack] is treated as it if was always
+    non-empty with [print_anomaly] as its bottom handler. *)
 
-let print e = print_gen !handle_stack e
+let where s =
+  if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
 
+let raw_anomaly e = match e with
+  | Util.Anomaly (s,pps) -> where s ++ pps ++ str "."
+  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
+  | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
 
-(*** Predefined handlers ***)
+let print_anomaly askreport e =
+  if askreport then
+    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+  else
+    hov 0 (raw_anomaly e)
 
-let where s =
-  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
+(** The standard exception printer *)
+let print e = print_gen (print_anomaly true) !handle_stack e
+
+(** Same as [print], except that the "Please report" part of an anomaly
+    isn't printed (used in Ltac debugging). *)
+let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+
+(** Same as [print], except that anomalies are not printed but re-raised
+    (used for the Fail command) *)
+let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
+
+(** Predefined handlers **)
 
 let _ = register_handler begin function
-  | Util.UserError(s,pps) ->
-      hov 0 (str "Error: " ++ where s ++ pps)
-  | Util.Anomaly (s,pps) ->
-      hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
+  | Util.UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps)
   | _ -> raise Unhandled
 end
 
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
diff --git a/lib/util.ml b/lib/util.ml
index 242c203211..5cd351237f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -19,8 +19,6 @@ exception UserError of string * std_ppcmds (* User errors *)
 let error string = raise (UserError(string, str string))
 let errorlabstrm l pps = raise (UserError(l,pps))
 
-exception AnomalyOnError of string * exn
-
 exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
 let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
diff --git a/lib/util.mli b/lib/util.mli
index 2216ba9813..baa1164897 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -27,8 +27,6 @@ val errorlabstrm : string -> std_ppcmds -> 'a
 exception AlreadyDeclared of std_ppcmds
 val alreadydeclared : std_ppcmds -> 'a
 
-exception AnomalyOnError of string * exn
-
 (** [todo] is for running of an incomplete code its implementation is
    "do nothing" (or print a message), but this function should not be
    used in a released code *)