summaryrefslogtreecommitdiff
path: root/toplevel/cerrors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/cerrors.ml')
-rw-r--r--toplevel/cerrors.ml152
1 files changed, 43 insertions, 109 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 86057b4b..5f2c3dbb 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -1,20 +1,18 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
+open Compat
open Pp
open Util
open Indtypes
open Type_errors
open Pretype_errors
open Indrec
-open Lexer
let print_loc loc =
if loc = dummy_loc then
@@ -25,86 +23,37 @@ let print_loc loc =
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
- | Stream.Failure ->
- hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
- | Stream.Error txt ->
- hov 0 (str "Syntax error: " ++ str txt ++ str ".")
- | Token.Error txt ->
- hov 0 (str "Syntax error: " ++ str txt ++ str ".")
- | Sys_error msg ->
- hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
- | UserError(s,pps) ->
- hov 0 (str "Error: " ++ where s ++ pps)
- | Out_of_memory ->
- hov 0 (str "Out of memory.")
- | Stack_overflow ->
- hov 0 (str "Stack overflow.")
- | Timeout ->
- hov 0 (str "Timeout!")
- | Anomaly (s,pps) ->
- hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
- | AnomalyOnError (s,exc) ->
- hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++
- fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
- | Match_failure(filename,pos1,pos2) ->
- hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++
- if Sys.ocaml_version = "3.06" then
- (str " from character " ++ int pos1 ++
- str " to " ++ int pos2)
- else
- (str " at line " ++ int pos1 ++
- str " character " ++ int pos2)
- ++ report_fn ())
- | Not_found ->
- hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ())
- | Failure s ->
- hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ())
- | Invalid_argument s ->
- hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
- | Sys.Break ->
- hov 0 (fnl () ++ str "User interrupt.")
- | Lexer.Error Illegal_character ->
- hov 0 (str "Syntax error: Illegal character.")
- | Lexer.Error Unterminated_comment ->
- hov 0 (str "Syntax error: Unterminated comment.")
- | Lexer.Error Unterminated_string ->
- hov 0 (str "Syntax error: Unterminated string.")
- | Lexer.Error Undefined_token ->
- hov 0 (str "Syntax error: Undefined token.")
- | Lexer.Error (Bad_token s) ->
- hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
- | Stdpp.Exc_located (loc,exc) ->
+(** Registration of generic errors
+ Nota: explain_exn does NOT end with a newline anymore!
+*)
+
+let explain_exn_default = function
+ (* Basic interaction exceptions *)
+ | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ "."))
+ | Token.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ "."))
+ | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
+ | 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!")
+ | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
+ (* Meta-exceptions *)
+ | 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
- if Sys.ocaml_version = "3.06" then
- (str ("(file \"" ^ s ^ "\", characters ") ++
- int b ++ str "-" ++ int e ++ str ")")
- else
- (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
- str ", characters " ++ int e ++ str "-" ++
- int (e+6) ++ str ")")
- else
- (mt ())) ++
- 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 ())
+ ++ Errors.print_no_anomaly exc)
+ | EvaluatedError (msg,None) -> msg
+ | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise
+ (* Otherwise, not handled here *)
+ | _ -> raise Errors.Unhandled
+
+let _ = Errors.register_handler explain_exn_default
+
+
+(** Pre-explain a vernac interpretation error *)
let wrap_vernac_error strm =
EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
@@ -120,13 +69,17 @@ let rec process_vernac_interp_error = function
mt() in
wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
- wrap_vernac_error (Himsg.explain_type_error ctx te)
- | PretypeError(ctx,te) ->
- wrap_vernac_error (Himsg.explain_pretype_error ctx te)
+ wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te)
+ | PretypeError(ctx,sigma,te) ->
+ wrap_vernac_error (Himsg.explain_pretype_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error (Himsg.explain_typeclass_error env te)
| InductiveError e ->
wrap_vernac_error (Himsg.explain_inductive_error e)
+ | Modops.ModuleTypingError e ->
+ wrap_vernac_error (Himsg.explain_module_error e)
+ | Modintern.ModuleInternalizationError e ->
+ wrap_vernac_error (Himsg.explain_module_internalization_error e)
| RecursionSchemeError e ->
wrap_vernac_error (Himsg.explain_recursion_scheme_error e)
| Cases.PatternMatchingError (env,e) ->
@@ -145,10 +98,10 @@ let rec process_vernac_interp_error = function
(str "No constant of this name:" ++ spc () ++
Libnames.pr_qualid q ++ str ".")
| Refiner.FailError (i,s) ->
- 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")."),
- None)
+ wrap_vernac_error
+ (str "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").")
| AlreadyDeclared msg ->
wrap_vernac_error (msg ++ str ".")
| Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
@@ -156,32 +109,13 @@ let rec process_vernac_interp_error = function
| Proof_type.LtacLocated (s,exc) ->
EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
Some (process_vernac_interp_error exc))
- | Stdpp.Exc_located (loc,exc) ->
- Stdpp.Exc_located (loc,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: "
-
-let report () = (str "." ++ spc () ++ str "Please report.")
-
-let explain_exn_default =
- explain_exn_default_aux anomaly_string report
-
-let raise_if_debug e =
- if !Flags.debug then raise e
-
let _ = Tactic_debug.explain_logic_error :=
- (fun e -> explain_exn_default (process_vernac_interp_error e))
+ (fun e -> Errors.print (process_vernac_interp_error e))
let _ = Tactic_debug.explain_logic_error_no_anomaly :=
- (fun e ->
- explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
- (process_vernac_interp_error e))
-
-let explain_exn_function = ref explain_exn_default
-
-let explain_exn e = !explain_exn_function e
-
-let explain_exn_no_anomaly e =
- explain_exn_default_aux (fun () -> raise e) mt e
+ (fun e -> Errors.print_no_report (process_vernac_interp_error e))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 16:08:58 +0000