From 2014b6b4153d034c4c0ee96de7b4fd20fb629492 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 12 Jul 2012 12:37:03 +0000
Subject: 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
---
 grammar/tacextend.ml4    |  6 +++++-
 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
-- 
cgit v1.2.3