diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/explainErr.ml | 75 | ||||
| -rw-r--r-- | vernac/explainErr.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
3 files changed, 38 insertions, 42 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index ec7333aa43..5c5a4ffbcb 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -44,57 +44,61 @@ let explain_exn_default = function let _ = CErrors.register_handler explain_exn_default -(** Pre-explain a vernac interpretation error *) - -let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) - -let process_vernac_interp_error exn = match fst exn with +let vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i + str "." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i else mt() in - wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") + str "Universe inconsistency" ++ msg ++ str "." | TypeError(ctx,te) -> - let te = map_ptype_error EConstr.of_constr te in - wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) + let te = map_ptype_error EConstr.of_constr te in + Himsg.explain_type_error ctx Evd.empty te | PretypeError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) + Himsg.explain_pretype_error ctx sigma te | Notation.PrimTokenNotationError(kind,ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te) + Himsg.explain_prim_token_notation_error kind ctx sigma te | Typeclasses_errors.TypeClassError(env, sigma, te) -> - wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te) + Himsg.explain_typeclass_error env sigma te | InductiveError e -> - wrap_vernac_error exn (Himsg.explain_inductive_error e) + Himsg.explain_inductive_error e | Modops.ModuleTypingError e -> - wrap_vernac_error exn (Himsg.explain_module_error e) + Himsg.explain_module_error e | Modintern.ModuleInternalizationError e -> - wrap_vernac_error exn (Himsg.explain_module_internalization_error e) + Himsg.explain_module_internalization_error e | RecursionSchemeError (env,e) -> - wrap_vernac_error exn (Himsg.explain_recursion_scheme_error env e) + Himsg.explain_recursion_scheme_error env e | Cases.PatternMatchingError (env,sigma,e) -> - wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) + Himsg.explain_pattern_matching_error env sigma e | Tacred.ReductionTacticError e -> - wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) + Himsg.explain_reduction_tactic_error e | Logic.RefinerError (env, sigma, e) -> - wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) + Himsg.explain_refiner_error env sigma e | Nametab.GlobalizationError q -> - wrap_vernac_error exn - (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment.") + str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment." | Refiner.FailError (i,s) -> - let s = Lazy.force s in - wrap_vernac_error exn - (str "Tactic failure" ++ - (if Pp.ismt s then s else str ": " ++ s) ++ - if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") + let s = Lazy.force s in + str "Tactic failure" ++ + (if Pp.ismt s then s else str ": " ++ s) ++ + if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")." | AlreadyDeclared msg -> - wrap_vernac_error exn (msg ++ str ".") + msg ++ str "." | _ -> - exn + raise CErrors.Unhandled + +let _ = CErrors.register_handler vernac_interp_error_handler + +(** Pre-explain a vernac interpretation error *) + +let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) + +let process_vernac_interp_error exn = + try vernac_interp_error_handler (fst exn) |> wrap_vernac_error exn + with CErrors.Unhandled -> exn let rec strip_wrapping_exceptions = function | Logic_monad.TacticFailure e -> @@ -106,16 +110,9 @@ let additional_error_info = ref [] let register_additional_error_info f = additional_error_info := f :: !additional_error_info -let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = +let process_vernac_interp_error (exc, info) = let exc = strip_wrapping_exceptions exc in let e = process_vernac_interp_error (exc, info) in - let () = - if not allow_uncaught && not (CErrors.handled (fst e)) then - let (e, info) = e in - let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in - let err = CErrors.make_anomaly msg in - Util.iraise (err, info) - in let e' = try Some (CList.find_map (fun f -> f e) !additional_error_info) with _ -> None diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli index eb956f2e60..cc2a130925 100644 --- a/vernac/explainErr.mli +++ b/vernac/explainErr.mli @@ -13,7 +13,7 @@ exception EvaluatedError of Pp.t * exn option (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn +val process_vernac_interp_error : Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ca7f7ffa0b..ac47a6a8f3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2308,8 +2308,7 @@ let with_fail ~st f = | HasNotFailed as e -> raise e | e when CErrors.noncritical e || e = Timeout -> let e = CErrors.push e in - raise (HasFailed (CErrors.iprint - (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) + raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error e))) with e when CErrors.noncritical e -> (* Restore the previous state XXX Careful here with the cache! *) Vernacstate.invalidate_cache (); |