diff options
Diffstat (limited to 'toplevel/cerrors.ml')
| -rw-r--r-- | toplevel/cerrors.ml | 46 |
1 files changed, 24 insertions, 22 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 22ea09c5..b29ba1ef 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Errors open Indtypes @@ -53,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 @@ -66,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 @@ -108,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 |