aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml4
-rw-r--r--lib/loc.ml16
-rw-r--r--lib/loc.mli16
-rw-r--r--parsing/compat.ml44
-rw-r--r--parsing/lexer.ml45
-rw-r--r--pretyping/cases.ml4
-rw-r--r--pretyping/pretype_errors.ml3
-rw-r--r--pretyping/typeclasses_errors.ml7
-rw-r--r--printing/ppvernac.ml4
-rw-r--r--proofs/logic.ml1
-rw-r--r--proofs/proofview.ml1
-rw-r--r--proofs/refiner.ml10
-rw-r--r--tactics/class_tactics.ml41
-rw-r--r--tactics/extratactics.ml47
-rw-r--r--tactics/rewrite.ml42
-rw-r--r--tactics/tacinterp.ml22
-rw-r--r--toplevel/cerrors.ml48
-rw-r--r--toplevel/ide_slave.ml11
-rw-r--r--toplevel/obligations.ml1
-rw-r--r--toplevel/toplevel.ml16
-rw-r--r--toplevel/vernac.ml7
-rw-r--r--toplevel/vernacentries.ml3
22 files changed, 101 insertions, 92 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 1daf449d8..5cfd71fbf 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -269,10 +269,6 @@ let rec explain_exn = function
(* let ctx = Check.get_env() in
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
- | Loc.Exc_located (loc, exc) ->
- hov 0 ((if loc = Loc.ghost then (mt ())
- else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
- ++ explain_exn exc)
| Assert_failure (s,b,e) ->
hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
(if s = "" then mt ()
diff --git a/lib/loc.ml b/lib/loc.ml
index e87ad132e..8f133ce0d 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -19,8 +19,6 @@ type t = {
ep : int; (** end position *)
}
-exception Exc_located of t * exn
-
let create fname line_nb bol_pos (bp, ep) = {
fname = fname; line_nb = line_nb; bol_pos = bol_pos;
line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
@@ -58,12 +56,22 @@ let unloc loc = (loc.bp, loc.ep)
let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep)
-let raise loc e = raise (Exc_located (loc, e))
-
let dummy_loc = ghost
let join_loc = merge
+(** Located type *)
+
type 'a located = t * 'a
let located_fold_left f x (_,a) = f x a
let located_iter2 f (_,a) (_,b) = f a b
let down_located f (_,a) = f a
+
+(** Exceptions *)
+
+let location : t Exninfo.t = Exninfo.make ()
+
+let add_loc e loc = Exninfo.add e location loc
+
+let get_loc e = Exninfo.get e location
+
+let raise loc e = raise (Exninfo.add e location loc)
diff --git a/lib/loc.mli b/lib/loc.mli
index c712cddd9..a0b99c689 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -10,8 +10,6 @@
type t
-exception Exc_located of t * exn
-
type 'a located = t * 'a
(** Embed a location in a type *)
@@ -37,12 +35,20 @@ val is_ghost : t -> bool
val merge : t -> t -> t
-val raise : t -> exn -> 'a
-(** Raise a located exception *)
-
val represent : t -> (string * int * int * int * int)
(** Return the arguments given in [create] *)
+(** {5 Located exceptions} *)
+
+val add_loc : exn -> t -> exn
+(** Adding location to an exception *)
+
+val get_loc : exn -> t option
+(** Retrieving the optional location of an exception *)
+
+val raise : t -> exn -> 'a
+(** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *)
+
(** {5 Location utilities} *)
val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 637b427a0..e82f35274 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -193,7 +193,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
let entry_create = Entry.create
let entry_parse e p =
try Entry.parse e p
- with Exc_located (loc,e) -> raise (Loc.Exc_located (to_coqloc loc,e))
+ with Exc_located (loc,e) -> raise (Loc.add_loc e (to_coqloc loc))
IFDEF CAMLP5_6_02_1 THEN
let entry_print ft x = Entry.print ft x
ELSE
@@ -221,7 +221,7 @@ end
module GrammarMake (L:LexerSig) : GrammarSig = struct
(* We need to refer to Coq's module Loc before it is hidden by include *)
- let raise_coq_loc loc e = raise (Loc.Exc_located (to_coqloc loc,e))
+ let raise_coq_loc loc e = raise (Loc.add_loc e (to_coqloc loc))
include Camlp4.Struct.Grammar.Static.Make (L)
type 'a entry = 'a Entry.t
type action = Action.t
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 4b3a3f3a1..91e7846dc 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -171,8 +171,9 @@ let lookup_utf8 cs =
| Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail c cs)
| None -> EmptyStream
-let unlocated f x =
- try f x with Loc.Exc_located (_, exc) -> raise exc
+let unlocated f x = f x
+ (** FIXME: should we still unloc the exception? *)
+(* try f x with Loc.Exc_located (_, exc) -> raise exc *)
let check_keyword str =
let rec loop_symb = parser
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2910774db..358cc2f03 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -69,9 +69,7 @@ let rec list_try_compile f = function
| [] -> anomaly (str "try_find_f")
| h::t ->
try f h
- with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _
- | Loc.Exc_located
- (_, (UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _)) ->
+ with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
list_try_compile f t
let force_name =
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 5403c1e99..91d24ec69 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -53,8 +53,7 @@ exception PretypeError of env * Evd.evar_map * pretype_error
let precatchable_exception = function
| Errors.UserError _ | TypeError _ | PretypeError _
- | Loc.Exc_located(_,(Errors.UserError _ | TypeError _ |
- Nametab.GlobalizationError _ | PretypeError _)) -> true
+ | Nametab.GlobalizationError _ -> true
| _ -> false
(* This simplifies the typing context of Cases clauses *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index cfcf9cf43..d0d90017f 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -39,14 +39,13 @@ let unsatisfiable_constraints env evd ev =
| None ->
raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
| Some ev ->
- let loc, kind = Evd.evar_source ev evd in
- raise (Loc.Exc_located (loc, TypeClassError
- (env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
+ let loc, kind = Evd.evar_source ev evd in
+ let err = TypeClassError (env, UnsatisfiableConstraints (evd, Some (ev, kind))) in
+ Loc.raise loc err
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
let rec unsatisfiable_exception exn =
match exn with
| TypeClassError (_, UnsatisfiableConstraints _) -> true
- | Loc.Exc_located(_, e) -> unsatisfiable_exception e
| _ -> false
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 14ca732a4..0082993b7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -769,9 +769,7 @@ let rec pr_vernac = function
| VernacSolve (i,tac,deftac) ->
(if i = 1 then mt() else int i ++ str ": ") ++
pr_raw_tactic tac
- ++ (try if deftac then str ".." else mt ()
- with UserError _|Loc.Exc_located _ -> mt())
-
+ ++ (if deftac then str ".." else mt ())
| VernacSolveExistential (i,c) ->
str"Existential " ++ int i ++ pr_lconstrarg c
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 80a2e1d1a..e2f698acd 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -41,7 +41,6 @@ exception RefinerError of refiner_error
open Pretype_errors
let rec catchable_exception = function
- | Loc.Exc_located(_,e) -> catchable_exception e
| LtacLocated(_,_,e) -> catchable_exception e
| Errors.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
| RefinerError _ | Indrec.RecursionSchemeError _
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 7b384b13e..1066c173b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -334,7 +334,6 @@ let tclEXTEND tacs1 rtac tacs2 env =
this should be maintained synchronized, probably. *)
open Pretype_errors
let rec catchable_exception = function
- | Loc.Exc_located(_,e) -> catchable_exception e
| Proof_type.LtacLocated(_,_,e) -> catchable_exception e
| Errors.UserError _
| Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 332f255b2..4592c60dd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -216,15 +216,15 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
let catch_failerror e =
if catchable_exception e then check_for_interrupt ()
else match e with
- | FailError (0,_) | Loc.Exc_located(_, FailError (0,_))
+ | FailError (0,_)
| LtacLocated (_,_,FailError (0,_)) ->
check_for_interrupt ()
- | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
- | Loc.Exc_located(s,FailError (lvl,s')) ->
- raise (Loc.Exc_located(s,FailError (lvl - 1, s')))
+ | FailError (lvl,s) ->
+ raise (Exninfo.copy e (FailError (lvl - 1, s)))
| LtacLocated (s'',loc,FailError (lvl,s')) ->
raise (LtacLocated (s'',loc,FailError (lvl - 1,s')))
| e -> raise e
+ (** FIXME: do we need to add a [Errors.push] here? *)
(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
let tclORELSE0 t1 t2 g =
@@ -325,7 +325,7 @@ let tclTIMEOUT n t g =
restore_timeout ();
res
with
- | TacTimeout | Loc.Exc_located(_,TacTimeout) ->
+ | TacTimeout ->
restore_timeout ();
errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!")
| e -> restore_timeout (); raise e
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c70351caa..329be18eb 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -195,7 +195,6 @@ let e_possible_resolve db_list local_db gl =
let rec catchable = function
| Refiner.FailError _ -> true
- | Loc.Exc_located (_, e) -> catchable e
| Proof_type.LtacLocated (_, _, e) -> catchable e
| e -> Logic.catchable_exception e
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f802788d4..7a8cccc6d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -596,9 +596,10 @@ let hResolve id c occ t gl =
let rec resolve_hole t_hole =
try
Pretyping.understand sigma env t_hole
- with
- | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) ->
- resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
+ with
+ | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
+ let loc = match Loc.get_loc e with None -> Loc.ghost | Some loc -> loc in
+ resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
in
let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
let t_constr_type = Retyping.get_type_of env sigma t_constr in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 8b0820c52..fbe11432e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1209,7 +1209,6 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
treat res
with
- | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
Refiner.tclFAIL 0
(str"Unable to satisfy the rewriting constraints."
@@ -1300,7 +1299,6 @@ let cl_rewrite_clause_newtac ?abs strat clause =
cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
in return (res, is_hyp)
with
- | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
++ fnl () ++ Himsg.explain_typeclass_error env e)))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 530f15f34..274a23559 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -73,8 +73,13 @@ let catch_error call_trace tac g =
let e = Errors.push e in
let inner_trace,loc,e = match e with
| LtacLocated (inner_trace,loc,e) -> inner_trace,loc,e
- | Loc.Exc_located (loc,e) -> [],loc,e
- | e -> [],Loc.ghost,e in
+ | e ->
+ let loc = match Loc.get_loc e with
+ | None -> Loc.ghost
+ | Some loc -> loc
+ in
+ [], loc, e
+ in
if List.is_empty call_trace & List.is_empty inner_trace then raise e
else
raise (LtacLocated(inner_trace@call_trace,loc,e))
@@ -1188,15 +1193,16 @@ and eval_with_fail ist is_lazy goal tac =
let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
VRTactic (catch_error trace tac { goal with sigma=sigma })
| a -> a)
- with
- | FailError (0,s) | Loc.Exc_located(_, FailError (0,s))
- | LtacLocated (_,_,FailError (0,s)) ->
+ with e ->
+ (** FIXME: Should we add [Errors.push]? *)
+ match e with
+ | FailError (0,s) | LtacLocated (_,_,FailError (0,s)) ->
raise (Eval_fail (Lazy.force s))
- | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
- | Loc.Exc_located(s,FailError (lvl,s')) ->
- raise (Loc.Exc_located(s,FailError (lvl - 1, s')))
+ | FailError (lvl,s) ->
+ raise (Exninfo.copy e (FailError (lvl - 1, s)))
| LtacLocated (s'',loc,FailError (lvl,s')) ->
raise (LtacLocated (s'',loc,FailError (lvl - 1, s')))
+ | _ -> raise e
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist gl llc u =
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 790520e97..ad7b70a6e 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -41,10 +41,10 @@ let explain_exn_default = function
| Timeout -> hov 0 (str "Timeout!")
| Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
(* Meta-exceptions *)
- | Loc.Exc_located (loc,exc) ->
+(* | Loc.Exc_located (loc,exc) ->
hov 0 ((if Loc.is_ghost loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
- ++ Errors.print_no_anomaly exc)
+ ++ Errors.print_no_anomaly exc)*)
| EvaluatedError (msg,None) -> msg
| EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise
(* Otherwise, not handled here *)
@@ -55,13 +55,14 @@ 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)
+let wrap_vernac_error exn strm =
+ let e = EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) in
+ Exninfo.copy exn e
let is_mt t =
Pervasives.(=) (Lazy.force t) (mt ()) (* FIXME *)
-let rec process_vernac_interp_error = function
+let rec process_vernac_interp_error exn = match exn with
| Univ.UniverseInconsistency (o,u,v,p) ->
let pr_rel r =
match r with
@@ -80,43 +81,43 @@ let rec process_vernac_interp_error = function
pr_rel o ++ spc() ++ Univ.pr_uni v ++ reason ++ str")"
else
mt() in
- wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
+ wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
- wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te)
+ wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
- wrap_vernac_error (Himsg.explain_pretype_error ctx sigma te)
+ wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
- wrap_vernac_error (Himsg.explain_typeclass_error env te)
+ wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
| InductiveError e ->
- wrap_vernac_error (Himsg.explain_inductive_error e)
+ wrap_vernac_error exn (Himsg.explain_inductive_error e)
| Modops.ModuleTypingError e ->
- wrap_vernac_error (Himsg.explain_module_error e)
+ wrap_vernac_error exn (Himsg.explain_module_error e)
| Modintern.ModuleInternalizationError e ->
- wrap_vernac_error (Himsg.explain_module_internalization_error e)
+ wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
| RecursionSchemeError e ->
- wrap_vernac_error (Himsg.explain_recursion_scheme_error e)
+ wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
| Cases.PatternMatchingError (env,e) ->
- wrap_vernac_error (Himsg.explain_pattern_matching_error env e)
+ wrap_vernac_error exn (Himsg.explain_pattern_matching_error env e)
| Tacred.ReductionTacticError e ->
- wrap_vernac_error (Himsg.explain_reduction_tactic_error e)
+ wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
| Logic.RefinerError e ->
- wrap_vernac_error (Himsg.explain_refiner_error e)
+ wrap_vernac_error exn (Himsg.explain_refiner_error e)
| Nametab.GlobalizationError q ->
- wrap_vernac_error
+ wrap_vernac_error exn
(str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
spc () ++ str "was not found" ++
spc () ++ str "in the current" ++ spc () ++ str "environment.")
| Nametab.GlobalizationConstantError q ->
- wrap_vernac_error
+ wrap_vernac_error exn
(str "No constant of this name:" ++ spc () ++
Libnames.pr_qualid q ++ str ".")
| Refiner.FailError (i,s) ->
- wrap_vernac_error
+ wrap_vernac_error exn
(str "Tactic failure" ++
(if not (is_mt s) then str ":" ++ Lazy.force s else mt ()) ++ (* FIXME *)
if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
| AlreadyDeclared msg ->
- wrap_vernac_error (msg ++ str ".")
+ wrap_vernac_error exn (msg ++ str ".")
| Proof_type.LtacLocated (_,_,(Refiner.FailError (i,s) as exc)) when not (is_mt s) ->
(* Ltac error is intended, trace is irrelevant *)
process_vernac_interp_error exc
@@ -124,10 +125,9 @@ let rec process_vernac_interp_error = function
(match
Himsg.extract_ltac_trace s loc (process_vernac_interp_error exc)
with
- | None,loc,e -> Loc.Exc_located (loc,e)
- | Some msg, loc, e -> Loc.Exc_located (loc,EvaluatedError (msg,Some e)))
- | Loc.Exc_located (loc,exc) ->
- Loc.Exc_located (loc,process_vernac_interp_error exc)
+ | None,loc,e -> Loc.add_loc e loc
+ | Some msg, loc, e ->
+ Loc.add_loc (EvaluatedError (msg,Some e)) loc)
| exc ->
exc
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index f16135dd7..98ba3e792 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -293,10 +293,13 @@ let eval_call c =
| Errors.Quit -> None, "Quit is not allowed by coqide!"
| Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
| Error_in_file (_,_,inner) -> None, pr_exn inner
- | Loc.Exc_located (loc, inner) ->
- let loc = if Loc.is_ghost loc then None else Some (Loc.unloc loc) in
- loc, pr_exn inner
- | e -> None, pr_exn e
+ | e ->
+ let loc = match Loc.get_loc e with
+ | None -> None
+ | Some loc ->
+ if Loc.is_ghost loc then None else Some (Loc.unloc loc)
+ in
+ loc, pr_exn e
in
let interruptible f x =
catch_break := true;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 7211417a6..b4384e77b 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -823,7 +823,6 @@ and solve_obligation_by_tac prg obls i tac =
let e = Errors.push e in
match e with
| Proof_type.LtacLocated (_, _, Refiner.FailError (_, s))
- | Loc.Exc_located(_, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
| e when Errors.is_anomaly e -> raise e
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index abdb3b74a..19cb22c13 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -263,7 +263,6 @@ let set_prompt prompt =
let rec is_pervasive_exn = function
| Out_of_memory | Stack_overflow | Sys.Break -> true
| Error_in_file (_,_,e) -> is_pervasive_exn e
- | Loc.Exc_located (_,e) -> is_pervasive_exn e
| DuringCommandInterp (_,e) -> is_pervasive_exn e
| _ -> false
@@ -279,15 +278,16 @@ let print_toplevel_error exc =
in
let (locstrm,exc) =
match exc with
- | Loc.Exc_located (loc, ie) ->
+ | Error_in_file (s, (inlibrary, fname, loc), ie) ->
+ (print_location_in_file s inlibrary fname loc, ie)
+ | ie ->
+ match Loc.get_loc ie with
+ | None -> (mt (), ie)
+ | Some loc ->
if valid_buffer_loc top_buffer dloc loc then
(print_highlight_location top_buffer loc, ie)
else
- ((mt ()) (* print_command_location top_buffer dloc *), ie)
- | Error_in_file (s, (inlibrary, fname, loc), ie) ->
- (print_location_in_file s inlibrary fname loc, ie)
- | _ ->
- ((mt ()) (* print_command_location top_buffer dloc *), exc)
+ (mt () (* print_command_location top_buffer dloc *), ie)
in
match exc with
| End_of_input ->
@@ -314,7 +314,7 @@ let parse_to_dot =
let rec discard_to_dot () =
try
Gram.entry_parse parse_to_dot top_buffer.tokens
- with Loc.Exc_located(_,(Compat.Token.Error _|Lexer.Error.E _)) ->
+ with (Compat.Token.Error _|Lexer.Error.E _) ->
discard_to_dot()
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index cb8962a9b..7ec19b26a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -106,14 +106,15 @@ let raise_with_file file exc =
match re with
| Error_in_file (_, (b,f,loc), e) when not (Loc.is_ghost loc) ->
((b, f, loc), e)
- | Loc.Exc_located (loc, e) when not (Loc.is_ghost loc) ->
+ | e ->
+ match Loc.get_loc e with
+ | Some loc when not (Loc.is_ghost loc) ->
((false,file, loc), e)
- | Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
+ | _ -> ((false,file,cmdloc), e)
in
raise (Error_in_file (file, inner, disable_drop inex))
let real_error = function
- | Loc.Exc_located (_, e) -> e
| Error_in_file (_, _, e) -> e
| e -> e
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4287db520..6b1055441 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1332,8 +1332,7 @@ let vernac_check_may_eval redexp glopt rc =
try
Evarutil.check_evars env sigma sigma' c;
Arguments_renaming.rename_typing env c
- with P.PretypeError (_,_,P.UnsolvableImplicit _)
- | Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) ->
+ with P.PretypeError (_,_,P.UnsolvableImplicit _) ->
Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
match redexp with
| None ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 18:27:36 +0000