diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 45 | ||||
| -rw-r--r-- | toplevel/cerrors.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
3 files changed, 29 insertions, 27 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 2df7c2273..b29ba1efc 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -52,12 +52,15 @@ let _ = Errors.register_handler explain_exn_default (** Pre-explain a vernac interpretation error *) -let wrap_vernac_error (exn, info) strm = - let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in - let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in - (e, info) +let wrap_vernac_error with_header (exn, info) strm = + if with_header then + let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in + let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in + (e, info) + else + (EvaluatedError (strm, None), info) -let process_vernac_interp_error exn = match fst exn with +let process_vernac_interp_error with_header exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then @@ -65,40 +68,40 @@ let process_vernac_interp_error exn = match fst exn with Univ.explain_universe_inconsistency Universes.pr_with_global_universes i else mt() in - wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") + wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) + wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) + wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> - wrap_vernac_error exn (Himsg.explain_typeclass_error env te) + wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te) | InductiveError e -> - wrap_vernac_error exn (Himsg.explain_inductive_error e) + wrap_vernac_error with_header exn (Himsg.explain_inductive_error e) | Modops.ModuleTypingError e -> - wrap_vernac_error exn (Himsg.explain_module_error e) + wrap_vernac_error with_header exn (Himsg.explain_module_error e) | Modintern.ModuleInternalizationError e -> - wrap_vernac_error exn (Himsg.explain_module_internalization_error e) + wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e) | RecursionSchemeError e -> - wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e) + wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,sigma,e) -> - wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) + wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> - wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) + wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - wrap_vernac_error exn (Himsg.explain_refiner_error e) + wrap_vernac_error with_header exn (Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> - wrap_vernac_error exn + wrap_vernac_error with_header exn (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 + wrap_vernac_error with_header exn (str "Tactic failure" ++ (if Pp.is_empty 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 ".") + wrap_vernac_error with_header exn (msg ++ str ".") | _ -> exn @@ -107,9 +110,9 @@ let rec strip_wrapping_exceptions = function strip_wrapping_exceptions e | exc -> exc -let process_vernac_interp_error (exc, info) = +let process_vernac_interp_error ?(with_header=true) (exc, info) = let exc = strip_wrapping_exceptions exc in - let e = process_vernac_interp_error (exc, info) in + let e = process_vernac_interp_error with_header (exc, info) in let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 1768af118..100b3772c 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : Util.iexn -> Util.iexn +val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1b8fdd8ae..52b4dc8cf 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2062,7 +2062,7 @@ let locate_if_not_already loc (e, info) = | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info) exception HasNotFailed -exception HasFailed of string +exception HasFailed of std_ppcmds let with_fail b f = if not b then f () @@ -2077,8 +2077,8 @@ let with_fail b f = | HasNotFailed as e -> raise e | e -> let e = Errors.push e in - raise (HasFailed (Pp.string_of_ppcmds - (Errors.iprint (Cerrors.process_vernac_interp_error e))))) + raise (HasFailed (Errors.iprint + (Cerrors.process_vernac_interp_error ~with_header:false e)))) () with e when Errors.noncritical e -> let (e, _) = Errors.push e in @@ -2087,8 +2087,7 @@ let with_fail b f = errorlabstrm "Fail" (str "The command has not failed!") | HasFailed msg -> if is_verbose () || !Flags.ide_slave then msg_info - (str "The command has indeed failed with message:" ++ - fnl () ++ str "=> " ++ hov 0 (str msg)) + (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end |