diff options
Diffstat (limited to 'toplevel/cerrors.ml')
| -rw-r--r-- | toplevel/cerrors.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index b29ba1ef..accba312 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -20,7 +20,7 @@ let print_loc loc = let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) -let guill s = "\""^s^"\"" +let guill s = str "\"" ++ str s ++ str "\"" (** Invariant : exceptions embedded in EvaluatedError satisfy Errors.noncritical *) @@ -33,10 +33,10 @@ exception EvaluatedError of std_ppcmds * exn option let explain_exn_default = function (* Basic interaction exceptions *) - | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) - | Compat.Token.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) + | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) - | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg)) + | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") | Timeout -> hov 0 (str "Timeout!") @@ -110,9 +110,16 @@ let rec strip_wrapping_exceptions = function strip_wrapping_exceptions e | exc -> exc -let process_vernac_interp_error ?(with_header=true) (exc, info) = +let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) = let exc = strip_wrapping_exceptions exc in let e = process_vernac_interp_error with_header (exc, info) in + let () = + if not allow_uncaught && not (Errors.handled (fst e)) then + let (e, info) = e in + let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in + let err = Errors.make_anomaly msg in + Util.iraise (err, 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 |