diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 17 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 6 | ||||
| -rw-r--r-- | toplevel/himsg.mli | 2 |
3 files changed, 13 insertions, 12 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index faf698d47..de4a614c9 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -23,6 +23,8 @@ let print_loc loc = let guill s = "\""^s^"\"" +(** Invariant : exceptions embedded in EvaluatedError satisfy + Errors.noncritical *) exception EvaluatedError of std_ppcmds * exn option @@ -40,9 +42,9 @@ let explain_exn_default = function | Stack_overflow -> hov 0 (str "Stack overflow.") | Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") - (* Meta-exceptions *) + (* Exceptions with pre-evaluated error messages *) | EvaluatedError (msg,None) -> msg - | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise + | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print reraise (* Otherwise, not handled here *) | _ -> raise Errors.Unhandled @@ -117,12 +119,11 @@ let rec process_vernac_interp_error exn = match exn with (* Ltac error is intended, trace is irrelevant *) process_vernac_interp_error exc | Proof_type.LtacLocated (s,loc,exc) -> - (match - Himsg.extract_ltac_trace s loc (process_vernac_interp_error exc) - with - | None,loc,e -> Loc.add_loc e loc - | Some msg, loc, e -> - Loc.add_loc (EvaluatedError (msg,Some e)) loc) + let e = process_vernac_interp_error exc in + assert (Errors.noncritical e); + (match Himsg.extract_ltac_trace s loc with + | None,loc -> Loc.add_loc e loc + | Some msg, loc -> Loc.add_loc (EvaluatedError (msg,Some e)) loc) | exc -> exc diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 87df8a055..2759c677b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1093,13 +1093,13 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = else mt () -let extract_ltac_trace trace eloc e = +let extract_ltac_trace trace eloc = let (nrep,loc,c),tail = List.sep_last trace in if is_defined_ltac trace then (* We entered a user-defined tactic, we display the trace with location of the call *) let msg = hov 0 (explain_ltac_call_trace (nrep,c,tail,eloc) ++ fnl()) in - Some msg, loc, e + Some msg, loc else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -1111,4 +1111,4 @@ let extract_ltac_trace trace eloc e = | _::tail -> aux tail | [] -> Loc.ghost in aux trace in - None, best_loc, e + None, best_loc diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index bd7fb8973..9ec344405 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -38,7 +38,7 @@ val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds val extract_ltac_trace : - Proof_type.ltac_trace -> Loc.t -> exn -> std_ppcmds option * Loc.t * exn + Proof_type.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t val explain_module_error : Modops.module_typing_error -> std_ppcmds |