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.ml | 64 +++++++++++++++++++++++++++++++++++------------------------
 1 file changed, 38 insertions(+), 26 deletions(-)

(limited to 'lib/errors.ml')

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
 
-- 
cgit v1.2.3