From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- toplevel/auto_ind_decl.ml | 44 +++++++++++++++++++++++++------------------- toplevel/autoinstance.ml | 3 ++- toplevel/backtrack.ml | 4 +++- toplevel/classes.ml | 11 ++++++++--- toplevel/coqinit.ml | 4 ++-- toplevel/coqtop.ml | 9 +++++---- toplevel/himsg.ml | 11 ++++++++--- toplevel/ide_intf.ml | 6 +++--- toplevel/ide_slave.ml | 11 ++++++----- toplevel/ind_tables.ml | 5 +++-- toplevel/indschemes.ml | 7 ++++--- toplevel/lemmas.ml | 27 ++++++++++++++++++--------- toplevel/metasyntax.ml | 13 +++++++++---- toplevel/mltop.ml4 | 11 ++++++----- toplevel/search.ml | 2 +- toplevel/toplevel.ml | 12 ++++++------ toplevel/vernac.ml | 24 ++++++++++++------------ toplevel/vernacentries.ml | 13 ++++++++----- toplevel/vernacinterp.ml | 4 ++-- 19 files changed, 131 insertions(+), 90 deletions(-) (limited to 'toplevel') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 3690b924..b9ab68ec 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -111,7 +111,7 @@ let mkFullInd ind n = let check_bool_is_defined () = try let _ = Global.type_of_global Coqlib.glob_bool in () - with _ -> raise (UndefinedCst "bool") + with e when Errors.noncritical e -> raise (UndefinedCst "bool") let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -304,8 +304,9 @@ let destruct_ind c = try let u,v = destApp c in let indc = destInd u in indc,v - with _-> let indc = destInd c in - indc,[||] + with e when Errors.noncritical e -> + let indc = destInd c in + indc,[||] (* In the following, avoid is the list of names to avoid. @@ -329,8 +330,9 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q = else error ("Var "^(string_of_id s)^" seems unknown.") ) in mkVar (find 1) - with _ -> (* if this happen then the args have to be already declared as a - Parameter*) + with e when Errors.noncritical e -> + (* if this happen then the args have to be already declared as a + Parameter*) ( let mp,dir,lbl = repr_con (destConst v) in mkConst (make_con mp dir (mk_label ( @@ -376,8 +378,9 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = else error ("Var "^(string_of_id s)^" seems unknown.") ) in mkVar (find 1) - with _ -> (* if this happen then the args have to be already declared as a - Parameter*) + with e when Errors.noncritical e -> + (* if this happen then the args have to be already declared as a + Parameter*) ( let mp,dir,lbl = repr_con (destConst v) in mkConst (make_con mp dir (mk_label ( @@ -394,7 +397,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = else ( let u,v = try destruct_ind tt1 (* trick so that the good sequence is returned*) - with _ -> ind,[||] + with e when Errors.noncritical e -> ind,[||] in if u = ind then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2) else ( @@ -427,17 +430,19 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt = | ([],[]) -> [] | _ -> error "Both side of the equality must have the same arity." in - let (ind1,ca1) = try destApp lft with - _ -> error "replace failed." - and (ind2,ca2) = try destApp rgt with - _ -> error "replace failed." + let (ind1,ca1) = + try destApp lft with e when Errors.noncritical e -> error "replace failed." + and (ind2,ca2) = + try destApp rgt with e when Errors.noncritical e -> error "replace failed." in - let (sp1,i1) = try destInd ind1 with - _ -> (try fst (destConstruct ind1) with _ -> - error "The expected type is an inductive one.") - and (sp2,i2) = try destInd ind2 with - _ -> (try fst (destConstruct ind2) with _ -> - error "The expected type is an inductive one.") + let (sp1,i1) = + try destInd ind1 with e when Errors.noncritical e -> + try fst (destConstruct ind1) with e when Errors.noncritical e -> + error "The expected type is an inductive one." + and (sp2,i2) = + try destInd ind2 with e when Errors.noncritical e -> + try fst (destConstruct ind2) with e when Errors.noncritical e -> + error "The expected type is an inductive one." in if (sp1 <> sp2) || (i1 <> i2) then (error "Eq should be on the same type") @@ -714,7 +719,8 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind (* Decidable equality *) let check_not_is_defined () = - try ignore (Coqlib.build_coq_not ()) with _ -> raise (UndefinedCst "not") + try ignore (Coqlib.build_coq_not ()) + with e when Errors.noncritical e -> raise (UndefinedCst "not") (* {n=m}+{n<>m} part *) let compute_dec_goal ind lnamesparrec nparrec = diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 10709abc..f43fc505 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -204,7 +204,8 @@ let declare_class_instance gr ctx params = (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst)); new_instance_message ident typ def - with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e) + with e when Errors.noncritical e -> + msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e) let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t; match kind_of_term t with diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 912d694e..f444fc2d 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -96,7 +96,9 @@ let mark_command ast = Stack.push { label = Lib.current_command_label (); nproofs = List.length (Pfedit.get_all_proof_names ()); - prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None); + prfname = + (try Some (Pfedit.get_current_proof_name ()) + with Proof_global.NoCurrentProof -> None); prfdepth = max 0 (Pfedit.current_proof_depth ()); reachable = true; ngoals = get_ngoals (); diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 6914b8f0..de4d1ab1 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -37,7 +37,10 @@ let set_typeclass_transparency c local b = let _ = Typeclasses.register_add_instance_hint (fun inst local pri -> - let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in + let path = + try Auto.PathHints [global_of_constr inst] + with e when Errors.noncritical e -> Auto.PathAny + in Flags.silently (fun () -> Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry @@ -300,8 +303,10 @@ let context l = let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; - let ctx = try named_of_rel_context fullctx with _ -> - error "Anonymous variables not allowed in contexts." + let ctx = + try named_of_rel_context fullctx + with e when Errors.noncritical e -> + error "Anonymous variables not allowed in contexts." in let fn (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 66a9516a..8f954573 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -46,9 +46,9 @@ let load_rcfile() = mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ " found. Skipping rcfile loading.")) *) - with e -> + with reraise -> (msgnl (str"Load of rcfile failed."); - raise e) + raise reraise) else Flags.if_verbose msgnl (str"Skipping rcfile loading.") diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index df388d1d..adbdb31b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -24,7 +24,8 @@ let get_version_date () = let ver = input_line ch in let rev = input_line ch in (ver,rev) - with _ -> (Coq_config.version,Coq_config.date) + with e when Errors.noncritical e -> + (Coq_config.version,Coq_config.date) let print_header () = let (ver,rev) = (get_version_date ()) in @@ -310,7 +311,7 @@ let parse_args arglist = with Stream.Failure -> msgnl (Errors.print e); exit 1 end - | e -> begin msgnl (Errors.print e); exit 1 end + | any -> begin msgnl (Errors.print any); exit 1 end let init arglist = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) @@ -344,10 +345,10 @@ let init arglist = load_vernacular (); compile_files (); outputstate () - with e -> + with any -> flush_all(); if not !batch_mode then message "Error during initialization:"; - msgnl (Toplevel.print_toplevel_error e); + msgnl (Toplevel.print_toplevel_error any); exit 1 end; if !batch_mode then diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e7b5a0f2..f550df16 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -28,6 +28,8 @@ open Logic open Printer open Glob_term open Evd +open Libnames +open Declarations let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) @@ -307,7 +309,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = let fixenv = make_all_name_different fixenv in let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in str"Recursive definition is:" ++ spc () ++ pvd ++ str "." - with _ -> mt ()) + with e when Errors.noncritical e -> mt ()) let explain_ill_typed_rec_body env sigma i names vdefj vargs = let vdefj = jv_nf_evar sigma vdefj in @@ -542,8 +544,11 @@ let explain_not_match_error = function str "types given to " ++ str (string_of_id id) ++ str " differ" | NotConvertibleBodyField -> str "the body of definitions differs" - | NotConvertibleTypeField -> - str "types differ" + | NotConvertibleTypeField (env, typ1, typ2) -> + str "expected type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++ + str "but found type" ++ spc () ++ + quote (Printer.safe_pr_lconstr_env env typ1) | NotSameConstructorNamesField -> str "constructor names differ" | NotSameInductiveNameInBlockField -> diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 28f97dc8..6937eeb8 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -89,8 +89,8 @@ let abstract_eval_call handler c = | Quit -> Obj.magic (handler.quit () : unit) | About -> Obj.magic (handler.about () : coq_info) in Good res - with e -> - let (l, str) = handler.handle_exn e in + with any -> + let (l, str) = handler.handle_exn any in Fail (l,str) (** * XML data marshalling *) @@ -275,7 +275,7 @@ let to_value f = function let loc_s = int_of_string (List.assoc "loc_s" attrs) in let loc_e = int_of_string (List.assoc "loc_e" attrs) in Some (loc_s, loc_e) - with _ -> None + with e when e <> Sys.Break -> None in let msg = raw_string l in Fail (loc, msg) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index d67b272e..6e9a0ee0 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -237,7 +237,7 @@ let status () = in let proof = try Some (Names.string_of_id (Proof_global.get_current_proof_name ())) - with _ -> None + with Proof_global.NoCurrentProof -> None in let allproofs = let l = Proof_global.get_all_proof_names () in @@ -259,7 +259,8 @@ let search flags = | (Interface.Name_Pattern s, b) :: l -> let regexp = try Str.regexp s - with _ -> Util.error ("Invalid regexp: " ^ s) + with e when Errors.noncritical e -> + Util.error ("Invalid regexp: " ^ s) in extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l | (Interface.Type_Pattern s, b) :: l -> @@ -454,12 +455,12 @@ let loop () = Xml_utils.print_xml !orig_stdout xml_answer; flush !orig_stdout done - with e -> - let msg = Printexc.to_string e in + with any -> + let msg = Printexc.to_string any in let r = "Fatal exception in coqtop:\n" ^ msg in pr_debug ("==> " ^ r); (try Xml_utils.print_xml !orig_stdout (fail r); flush !orig_stdout - with _ -> ()); + with any -> ()); exit 1 diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 9f1a0218..77cfa6fa 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -86,8 +86,9 @@ let scheme_object_table = (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) let declare_scheme_object s aux f = - (try check_ident ("ind"^s) with _ -> - error ("Illegal induction scheme suffix: "^s)); + (try check_ident ("ind"^s) + with e when Errors.noncritical e -> + error ("Illegal induction scheme suffix: "^s)); let key = if aux = "" then s else aux in try let _ = Hashtbl.find scheme_object_table key in diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index fa6885af..e30404e1 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -159,7 +159,7 @@ let try_declare_scheme what f internal names kn = (strbrk "Required constant " ++ str s ++ str " undefined.") | AlreadyDeclared msg -> alarm what internal (msg ++ str ".") - | _ -> + | e when Errors.noncritical e -> alarm what internal (str "Unknown exception during scheme creation.") @@ -245,7 +245,8 @@ let try_declare_eq_decidability kn = let declare_eq_decidability = declare_eq_decidability_scheme_with [] -let ignore_error f x = try ignore (f x) with _ -> () +let ignore_error f x = + try ignore (f x) with e when Errors.noncritical e -> () let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin @@ -266,7 +267,7 @@ let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true - with _ -> false + with e when Errors.noncritical e -> false then ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index d6ab44c6..30f07fed 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -229,23 +229,32 @@ let get_proof opacity = id,{const with const_entry_opaque = opacity},do_guard,persistence,hook let save_named opacity = - let id,const,do_guard,persistence,hook = get_proof opacity in - save id const do_guard persistence hook + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + let id,const,do_guard,persistence,hook = get_proof opacity in + save id const do_guard persistence hook + end let check_anonymity id save_ident = if atompart_of_id id <> string_of_id (default_thm_id) then error "This command can only be used for unnamed theorem." let save_anonymous opacity save_ident = - let id,const,do_guard,persistence,hook = get_proof opacity in - check_anonymity id save_ident; - save save_ident const do_guard persistence hook + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + let id,const,do_guard,persistence,hook = get_proof opacity in + check_anonymity id save_ident; + save save_ident const do_guard persistence hook + end let save_anonymous_with_strength kind opacity save_ident = - let id,const,do_guard,_,hook = get_proof opacity in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save save_ident const do_guard (Global, Proof kind) hook + let p = Proof_global.give_me_the_proof () in + Proof.transaction p begin fun () -> + let id,const,do_guard,_,hook = get_proof opacity in + check_anonymity id save_ident; + (* we consider that non opaque behaves as local for discharge *) + save save_ident const do_guard (Global, Proof kind) hook + end (* Starting a goal *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 775a3af4..006dc5ec 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -237,7 +237,7 @@ let parse_format (loc,str) = | _ -> error "Box closed without being opened in format." else error "Empty format." - with e -> + with e when Errors.noncritical e -> Loc.raise loc e (***********************) @@ -277,6 +277,9 @@ let split_notation_string str = let out_nt = function NonTerminal x -> x | _ -> assert false +let msg_expected_form_of_recursive_notation = + "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"." + let rec find_pattern nt xl = function | Break n as x :: l, Break n' :: l' when n=n' -> find_pattern nt (x::xl) (l,l') @@ -289,13 +292,14 @@ let rec find_pattern nt xl = function | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | _, [] -> - error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") + error msg_expected_form_of_recursive_notation | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> anomaly "Only Terminal or Break expected on left, non-SProdList on right" let rec interp_list_parser hd = function | [] -> [], List.rev hd | NonTerminal id :: tl when id = ldots_var -> + if hd = [] then error msg_expected_form_of_recursive_notation; let hd = List.rev hd in let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in let xyl,tl'' = interp_list_parser [] tl' in @@ -337,7 +341,8 @@ let rec raw_analyze_notation_tokens = function let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with | ([Terminal "-"; Terminal x] | [Terminal x]) -> - (try let _ = Bigint.of_string x in true with _ -> false) + (try let _ = Bigint.of_string x in true + with e when Errors.noncritical e -> false) | _ -> false @@ -995,7 +1000,7 @@ let inNotation : notation_obj -> obj = let with_lib_stk_protection f x = let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a - with e -> Lib.unfreeze fs; raise e + with reraise -> Lib.unfreeze fs; raise reraise let with_syntax_protection f x = with_lib_stk_protection diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 2059ca60..f08308d3 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -92,8 +92,9 @@ let dir_ml_load s = (try t.load_obj s with | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u - | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ - str s ++ str" to Coq code.")) + | e when Errors.noncritical e -> + errorlabstrm "Mltop.load_object" + (str"Cannot link ml-object " ++ str s ++ str" to Coq code.")) (* TO DO: .cma loading without toplevel *) | WithoutTop -> IFDEF HasDynlink THEN @@ -142,7 +143,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.id_of_string d - with _ -> + with e when Errors.noncritical e -> if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); flush_all (); @@ -269,9 +270,9 @@ let if_verbose_load verb f name fname = try f name fname; msgnl (str (info^" done]")); - with e -> + with reraise -> msgnl (str (info^" failed]")); - raise e + raise reraise (** Load a module for the first time (i.e. dynlink it) or simulate its reload (i.e. doing nothing except maybe diff --git a/toplevel/search.ml b/toplevel/search.ml index 3e182689..19d696a1 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -137,7 +137,7 @@ let pattern_filter pat _ a c = try try is_matching pat (head c) - with _ -> + with e when Errors.noncritical e -> is_matching pat (head (Typing.type_of (Global.env()) Evd.empty c)) with UserError _ -> diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index d5321623..cc659e36 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -180,7 +180,7 @@ let print_location_in_file s inlibrary fname loc = str", line " ++ int line ++ str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () - with e -> + with e when Errors.noncritical e -> (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) @@ -208,7 +208,7 @@ let valid_buffer_loc ib dloc loc = let make_prompt () = try (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < " - with _ -> + with Proof_global.NoCurrentProof -> "Coq < " (*let build_pending_list l = @@ -340,7 +340,7 @@ let process_error = function discard_to_dot (); e with | End_of_input -> End_of_input - | de -> if is_pervasive_exn de then de else e + | any -> if is_pervasive_exn any then any else e (* do_vernac reads and executes a toplevel phrase, and print error messages when an exception is raised, except for the following: @@ -354,8 +354,8 @@ let do_vernac () = begin try raw_do_vernac top_buffer.tokens - with e -> - msgnl (print_toplevel_error (process_error e)) + with any -> + msgnl (print_toplevel_error (process_error any)) end; flush_all() @@ -374,6 +374,6 @@ let rec loop () = | Vernacexpr.Drop -> () | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Vernacexpr.Quit -> exit 0 - | e -> + | any -> msgerrnl (str"Anomaly. Please report."); loop () diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3314e82c..ed8e215f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -156,7 +156,7 @@ let close_input in_chan (_,verb) = match verb with | Some verb_ch -> close_in verb_ch | _ -> () - with _ -> () + with e when Errors.noncritical e -> () let verbose_phrase verbch loc = let loc = unloc loc in @@ -232,13 +232,13 @@ let rec vernac_com interpfun checknav (loc,com) = Lexer.restore_com_state cs; Pp.comments := cl; Dumpglob.coqdoc_unfreeze cds - with e -> + with reraise -> if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; Lexer.restore_com_state cs; Pp.comments := cl; Dumpglob.coqdoc_unfreeze cds; - raise e + raise reraise end | VernacList l -> List.iter (fun (_,v) -> interp v) l @@ -250,7 +250,7 @@ let rec vernac_com interpfun checknav (loc,com) = (* If the command actually works, ignore its effects on the state *) States.with_state_protection (fun v -> interp v; raise HasNotFailed) v - with e -> match real_error e with + with e when Errors.noncritical e -> match real_error e with | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed !") | e -> @@ -278,16 +278,16 @@ let rec vernac_com interpfun checknav (loc,com) = States.with_heavy_rollback interpfun Cerrors.process_vernac_interp_error v; restore_timeout psh - with e -> restore_timeout psh; raise e + with reraise -> restore_timeout psh; raise reraise in try checknav loc com; current_timeout := !default_timeout; if do_beautify () then pr_new_syntax loc (Some com); interp com - with e -> + with any -> Format.set_formatter_out_channel stdout; - raise (DuringCommandInterp (loc, e)) + raise (DuringCommandInterp (loc, any)) and read_vernac_file verbosely s = Flags.make_warn verbosely; @@ -316,13 +316,13 @@ and read_vernac_file verbosely s = end_inner_command (snd loc_ast); pp_flush () done - with e -> (* whatever the exception *) + with reraise -> (* whatever the exception *) Format.set_formatter_out_channel stdout; close_input in_chan input; (* we must close the file first *) - match real_error e with + match real_error reraise with | End_of_input -> if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None - | _ -> raise_with_file fname e + | _ -> raise_with_file fname reraise (** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit] It executes one vernacular command. By default the command is @@ -359,9 +359,9 @@ let load_vernac verb file = Lib.mark_end_of_command (); (* in case we're still in coqtop init *) read_vernac_file verb file; if !Flags.beautify_file then close_out !chan_beautify; - with e -> + with reraise -> if !Flags.beautify_file then close_out !chan_beautify; - raise_with_file file e + raise_with_file file reraise (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6618b695..75efe139 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -295,7 +295,7 @@ let dump_universes_gen g s = close (); msgnl (str ("Universes written to file \""^s^"\".")) with - e -> close (); raise e + reraise -> close (); raise reraise let dump_universes sorted s = let g = Global.universes () in @@ -331,7 +331,7 @@ let msg_notfound_library loc qid = function let print_located_library r = let (loc,qid) = qualid_of_reference r in try msg_found_library (Library.locate_qualified_library false qid) - with e -> msg_notfound_library loc qid e + with e when Errors.noncritical e -> msg_notfound_library loc qid e let print_located_module r = let (loc,qid) = qualid_of_reference r in @@ -364,7 +364,7 @@ let dump_global r = try let gr = Smartlocate.smart_global r in Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr - with _ -> () + with e when Errors.noncritical e -> () (**********) (* Syntax *) @@ -388,6 +388,7 @@ let vernac_notation = Metasyntax.add_notation (* Gallina *) let start_proof_and_print k l hook = + check_locality (); (* early check, cf #2975 *) start_proof_com k l hook; print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () @@ -910,7 +911,9 @@ let vernac_declare_arguments local r l nargs flags = | None -> None | Some (o, k) -> try Some(ignore(Notation.find_scope k); k) - with _ -> Some (Notation.find_delimiters_scope o k)) scopes in + with e when Errors.noncritical e -> + Some (Notation.find_delimiters_scope o k)) scopes + in let some_scopes_specified = List.exists ((<>) None) scopes in let rargs = Util.list_map_filter (function (n, true) -> Some n | _ -> None) @@ -1417,7 +1420,7 @@ let vernac_reset_name id = let gr = Smartlocate.global_with_alias (Ident id) in Dumpglob.add_glob (fst id) gr; true - with _ -> false in + with e when Errors.noncritical e -> false in if not globalized then begin try begin match Lib.find_opening_node (snd id) with diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index c4cc4ae5..a1b76d3d 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -60,7 +60,7 @@ let call (opn,converted_args) = hunk() with | Drop -> raise Drop - | e -> + | reraise -> if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); - raise e + raise reraise -- cgit v1.2.3