diff options
Diffstat (limited to 'toplevel/cerrors.ml')
| -rw-r--r-- | toplevel/cerrors.ml | 91 |
1 files changed, 51 insertions, 40 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 0d2111f8a..a34afda50 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -26,6 +26,8 @@ let guill s = "\""^s^"\"" let where s = if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) +exception EvaluatedError of std_ppcmds * exn option + (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) let rec explain_exn_default_aux anomaly_string report_fn = function @@ -63,6 +65,26 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") + | Assert_failure (s,b,e) -> + hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ + (if s = "" then mt () + else + (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ + str ", characters " ++ int e ++ str "-" ++ + int (e+6) ++ str ")")) ++ + report_fn ()) + | EvaluatedError (msg,None) -> + msg + | EvaluatedError (msg,Some reraise) -> + msg ++ explain_exn_default_aux anomaly_string report_fn reraise + | reraise -> + hov 0 (anomaly_string () ++ str "Uncaught exception " ++ + str (Printexc.to_string reraise) ++ report_fn ()) + +let wrap_vernac_error strm = + EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) + +let rec process_vernac_interp_error = function | Univ.UniverseInconsistency (o,u,v) -> let msg = if !Constrextern.print_universes then @@ -71,59 +93,48 @@ let rec explain_exn_default_aux anomaly_string report_fn = function ++ spc() ++ Univ.pr_uni v ++ str")" else mt() in - hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") + wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te) + wrap_vernac_error (Himsg.explain_type_error ctx te) | PretypeError(ctx,te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te) + wrap_vernac_error (Himsg.explain_pretype_error ctx te) | Typeclasses_errors.TypeClassError(env, te) -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te) + wrap_vernac_error (Himsg.explain_typeclass_error env te) | InductiveError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) + wrap_vernac_error (Himsg.explain_inductive_error e) | RecursionSchemeError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) - | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> - explain_exn_default_aux anomaly_string report_fn exc - | Proof_type.LtacLocated (s,exc) -> - hov 0 (Himsg.explain_ltac_call_trace s ++ fnl () - ++ explain_exn_default_aux anomaly_string report_fn exc) + wrap_vernac_error (Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,e) -> - hov 0 - (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) + wrap_vernac_error (Himsg.explain_pattern_matching_error env e) | Tacred.ReductionTacticError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e) + wrap_vernac_error (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e) + wrap_vernac_error (Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> - hov 0 (str "Error:" ++ spc () ++ - str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment.") + wrap_vernac_error + (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment.") | Nametab.GlobalizationConstantError q -> - hov 0 (str "Error:" ++ spc () ++ - str "No constant of this name:" ++ spc () ++ - Libnames.pr_qualid q ++ str ".") + wrap_vernac_error + (str "No constant of this name:" ++ spc () ++ + Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> - hov 0 (str "Error: Tactic failure" ++ + EvaluatedError (hov 0 (str "Error: Tactic failure" ++ (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ - if i=0 then str "." else str " (level " ++ int i ++ str").") - | 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 () - else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ - str ", characters " ++ int e ++ str "-" ++ - int (e+6) ++ str ")")) ++ - report_fn ()) + if i=0 then str "." else str " (level " ++ int i ++ str")."), + None) | AlreadyDeclared msg -> - hov 0 (str "Error: " ++ msg ++ str ".") - | reraise -> - hov 0 (anomaly_string () ++ str "Uncaught exception " ++ - str (Printexc.to_string reraise) ++ report_fn ()) + wrap_vernac_error (msg ++ str ".") + | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> + process_vernac_interp_error exc + | Proof_type.LtacLocated (s,exc) -> + EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()), + Some (process_vernac_interp_error exc)) + | Loc.Exc_located (loc,exc) -> + Loc.Exc_located (loc,process_vernac_interp_error exc) + | exc -> + exc let anomaly_string () = str "Anomaly: " |