diff options
| author | letouzey | 2012-07-12 12:37:03 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-12 12:37:03 +0000 |
| commit | 2014b6b4153d034c4c0ee96de7b4fd20fb629492 (patch) | |
| tree | 7d3f92abf0d07b30b735dfdb78d9faae853bcbc1 | |
| parent | b11b5c76df4f9fc2de050a3e9385b5f57550a394 (diff) | |
Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)
If an EXTEND block triggers an exception, the current behavior
is to print the exception (with Errors.print) ... and continue
as if nothing happened.
It's tempting to stop ignoring this exception, but that would currently
break ssreflect. For the moment, we simply display a nicer message
as suggested in bug #2797:
- the message starts with Warning instead of Error, and ends with a \n
- it also embeds the name of the concerned EXTEND block
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15607 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | grammar/tacextend.ml4 | 6 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 11 |
2 files changed, 13 insertions, 4 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 8f70302a0d..41c3676896 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -189,7 +189,11 @@ let declare_tactic loc s cl = Tacexpr.TacExtend($default_loc$,$se$,l))) | None -> () ]) $atomic_tactics$ - with e -> Pp.pp (Errors.print e); + with e -> + Pp.msg_warning + (Stream.iapp + (Pp.str ("Exception in tactic extend " ^ $se$ ^": ")) + (Errors.print e)); Egramml.extend_tactic_grammar $se$ $gl$; List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >> ]) diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 8ec189e3d1..2c9bc2675a 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -50,13 +50,18 @@ let mlexpr_of_clause = (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) let declare_command loc s nt cl = + let se = mlexpr_of_string s in let gl = mlexpr_of_clause cl in let funcl = make_fun_clauses loc s cl in declare_str_items loc [ <:str_item< do { - try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ - with e -> Pp.pp (Errors.print e); - Egramml.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ + try Vernacinterp.vinterp_add $se$ $funcl$ + with e -> + Pp.msg_warning + (Stream.iapp + (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) + (Errors.print e)); + Egramml.extend_vernac_command_grammar $se$ $nt$ $gl$ } >> ] open Pcaml |