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

8 files changed, 89 insertions, 113 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 *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3012cbae2f..1450d50322 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2982,7 +2982,9 @@ let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t))
 let tacticIn t =
   globTacticIn (fun ist ->
     try glob_tactic (t ist)
-    with e -> raise (AnomalyOnError ("Incorrect tactic expression", e)))
+    with e -> anomalylabstrm "tacticIn"
+      (str "Incorrect tactic expression. Received exception is:" ++
+       Errors.print e))
 
 let tacticOut = function
   | TacArg (TacDynamic (_,d)) ->
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 6124078562..5f2c3dbbe0 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -26,62 +26,35 @@ let guill s = "\""^s^"\""
 
 exception EvaluatedError of std_ppcmds * exn option
 
-(* Is an exception due to a regular user error, or to some
-   anomaly on the Coq side ? *)
+(** Registration of generic errors
+    Nota: explain_exn does NOT end with a newline anymore!
+*)
 
-let rec is_user_error = function
-  | Loc.Exc_located (_,e) -> is_user_error e
-  | EvaluatedError (_,Some e) -> is_user_error e
-  | EvaluatedError (_,None)
-  | Stream.Error _ | Token.Error _ | Lexer.Error.E _
-  | Sys_error _ | Out_of_memory | Stack_overflow | Timeout | Sys.Break
-  | UserError _ -> true
-  | _ -> false
-
-(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
-
-let rec explain_exn_default_aux anomaly_string report_fn = function
+let explain_exn_default = function
   (* Basic interaction exceptions *)
-  | Stream.Error txt ->
-      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
-  | Token.Error txt ->
-      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
-  | Lexer.Error.E err ->
-      hov 0 (str (Lexer.Error.to_string err))
-  | Sys_error msg ->
-      hov 0 (str "System error: " ++ str (guill msg))
-  | Out_of_memory ->
-      hov 0 (str "Out of memory.")
-  | Stack_overflow ->
-      hov 0 (str "Stack overflow.")
-  | Timeout ->
-      hov 0 (str "Timeout!")
-  | Sys.Break ->
-      hov 0 (fnl () ++ str "User interrupt.")
-  (* Variants of anomaly *)
-  | AnomalyOnError (s,exc) ->
-      hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++
-	fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
-  | Assert_failure (s,b,e) ->
-      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
-	       (if s = "" then mt ()
-		else
-		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
-		   str ", characters " ++ int e ++ str "-" ++
-		   int (e+6) ++ str ")")) ++
-	       report_fn ())
+  | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ "."))
+  | Token.Error txt ->  hov 0 (str ("Syntax error: " ^ txt ^ "."))
+  | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
+  | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg))
+  | Out_of_memory -> hov 0 (str "Out of memory.")
+  | Stack_overflow -> hov 0 (str "Stack overflow.")
+  | Timeout -> hov 0 (str "Timeout!")
+  | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
   (* Meta-exceptions *)
   | Loc.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
-               ++ explain_exn_default_aux anomaly_string report_fn exc)
-  | EvaluatedError (msg,None) ->
-      msg
-  | EvaluatedError (msg,Some reraise) ->
-      msg ++ explain_exn_default_aux anomaly_string report_fn reraise
+               ++ Errors.print_no_anomaly exc)
+  | EvaluatedError (msg,None) -> msg
+  | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise
   (* Otherwise, not handled here *)
   | _ -> raise Errors.Unhandled
 
+let _ = Errors.register_handler explain_exn_default
+
+
+(** Pre-explain a vernac interpretation error *)
+
 let wrap_vernac_error strm =
   EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
 
@@ -125,10 +98,10 @@ let rec process_vernac_interp_error = function
         (str "No constant of this name:" ++ spc () ++
          Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
-      EvaluatedError (hov 0 (str "Error: Tactic failure" ++
-                (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
-                if i=0 then str "." else str " (level " ++ int i ++ str")."),
-                None)
+      wrap_vernac_error
+	(str "Tactic failure" ++
+           (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
+           if i=0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
       wrap_vernac_error (msg ++ str ".")
   | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
@@ -141,24 +114,8 @@ let rec process_vernac_interp_error = function
   | exc ->
       exc
 
-let anomaly_string () = str "Anomaly: "
-
-let report () = (str "." ++ spc () ++ str "Please report.")
-
-let explain_exn_default =
-  explain_exn_default_aux anomaly_string report
-
-let raise_if_debug e =
-  if !Flags.debug then raise e
-
 let _ = Tactic_debug.explain_logic_error :=
-  (fun e -> explain_exn_default (process_vernac_interp_error e))
+  (fun e -> Errors.print (process_vernac_interp_error e))
 
 let _ = Tactic_debug.explain_logic_error_no_anomaly :=
-  (fun e ->
-    explain_exn_default_aux mt (fun () -> str ".")
-      (process_vernac_interp_error e))
-
-let explain_exn_function = ref explain_exn_default
-
-let _ = Errors.register_handler explain_exn_default
+  (fun e -> Errors.print_no_report (process_vernac_interp_error e))
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index feeada9254..da9d3590f5 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -13,18 +13,12 @@ open Util
 
 val print_loc : loc -> std_ppcmds
 
-(** Is an exception due to a regular user error, or to some
-    anomaly on the Coq side ? *)
-
-val is_user_error : exn -> bool
-
 (** Pre-explain a vernac interpretation error *)
 
 val process_vernac_interp_error : exn -> exn
 
-(** For debugging purpose (?), the explain function can be twicked *)
+(** General explain function. Should not be used directly now,
+    see instead function [Errors.print] and variants *)
 
-val explain_exn_function : (exn -> std_ppcmds) ref
 val explain_exn_default : exn -> std_ppcmds
 
-val raise_if_debug : exn -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ce9ca762df..87e0ebe17a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -209,11 +209,12 @@ let rec vernac_com interpfun (loc,com) =
 	with e -> match real_error e with
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed !")
-	  | e when Cerrors.is_user_error e ->
+	  | e ->
+	      (* Anomalies are re-raised by the next line *)
+	      let msg = Errors.print_no_anomaly e in
 	      if_verbose msgnl
 		(str "The command has indeed failed with message:" ++
-		 fnl () ++ str "=> " ++ hov 0 (Errors.print e))
-	  | _ -> raise e (* Anomalies are not catched by Fail *)
+		 fnl () ++ str "=> " ++ hov 0 msg)
 	end
 
     | VernacTime v ->