diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-16 18:01:26 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-16 18:01:26 +0000 |
commit | e9820ad33cd3ba4d34f7b51ffcf19216f4104ccc (patch) | |
tree | 719cf47df7bb93615a8a40dff407efc0945ef38a | |
parent | a343907e8c60ac3a33de6660de243c5beb9aeaa3 (diff) |
Repair the "Fail" command after recent changes in exception handling
For that, I introduce a explicit classification function
is_user_error : exn -> bool, instead of the previous hack
of explain_exn_default_aux (fun () -> raise e).
By the way, clean a bit explain_exn_default_aux : many cases
are just printed fine by default's Printexn.to_string (for example
Not_found).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14129 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | toplevel/cerrors.ml | 49 | ||||
-rw-r--r-- | toplevel/cerrors.mli | 9 | ||||
-rw-r--r-- | toplevel/vernac.ml | 10 |
3 files changed, 33 insertions, 35 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index ae09b202d..612407856 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -26,16 +26,28 @@ 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 ? *) + +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 - | Stream.Failure -> - hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") + (* 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)) + | 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 -> @@ -44,25 +56,12 @@ let rec explain_exn_default_aux anomaly_string report_fn = function 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) - | Match_failure(filename,pos1,pos2) -> - hov 0 (anomaly_string () ++ str "Match failure in file " ++ - str (guill filename) ++ str " at line " ++ int pos1 ++ - str " character " ++ int pos2 ++ report_fn ()) - | Not_found -> - hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ()) - | Failure s -> - hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ()) - | Invalid_argument s -> - hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) - | Sys.Break -> - hov 0 (fnl () ++ str "User interrupt.") - | 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) | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () @@ -71,10 +70,16 @@ let rec explain_exn_default_aux anomaly_string report_fn = function str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report_fn ()) + (* 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 + (* Otherwise, not handled here *) | _ -> raise Errors.Unhandled let wrap_vernac_error strm = @@ -156,8 +161,4 @@ let _ = Tactic_debug.explain_logic_error_no_anomaly := let explain_exn_function = ref explain_exn_default -let explain_exn e = !explain_exn_function e -let _ = Errors.register_handler explain_exn - -let explain_exn_no_anomaly e = - explain_exn_default_aux (fun () -> raise e) mt e +let _ = Errors.register_handler explain_exn_default diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 2670160ab..feeada925 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -13,13 +13,10 @@ open Util val print_loc : loc -> std_ppcmds -(* -val explain_exn : exn -> std_ppcmds -*) +(** Is an exception due to a regular user error, or to some + anomaly on the Coq side ? *) -(** Precompute errors raised during vernac interpretation *) - -val explain_exn_no_anomaly : exn -> std_ppcmds +val is_user_error : exn -> bool (** Pre-explain a vernac interpretation error *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index e77dba790..ce9ca762d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -209,11 +209,11 @@ let rec vernac_com interpfun (loc,com) = with e -> match real_error e with | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed !") - | e -> - (* if [e] is an anomaly, the next function will re-raise it *) - let msg = Cerrors.explain_exn_no_anomaly e in - if_verbose msgnl (str "The command has indeed failed with message:" ++ - fnl () ++ str "=> " ++ hov 0 msg) + | e when Cerrors.is_user_error e -> + 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 *) end | VernacTime v -> |