Ajout r gle d'affichage tactiques èéfinies par Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4409 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 37 insertions, 3 deletions

diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 091f98424c..caa144ce99 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -50,3 +50,6 @@ val reset_extend_grammars_v8 : unit -> unit
 
 val subst_all_grammar_command :
   Names.substitution -> all_grammar_command -> all_grammar_command
+
+val interp_entry_name : string -> string -> 
+  entry_type * Token.t Gramext.g_symbol
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4df5c8d206..88ba115867 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -137,9 +137,40 @@ let (inToken, outToken) =
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
-(* Grammar rules *)
-let cache_grammar (_,a) = Egrammar.extend_grammar a
-let subst_grammar (_,subst,a) = Egrammar.subst_all_grammar_command subst a
+(* Grammars (especially Tactic Notation) *)
+
+let make_terminal_status = function
+  | VTerm s -> Some s
+  | VNonTerm _ -> None
+
+let qualified_nterm current_univ = function
+  | NtQual (univ, en) -> (univ, en)
+  | NtShort en -> (current_univ, en)
+
+let rec make_tags = function
+  | VTerm s :: l -> make_tags l
+  | VNonTerm (loc, nt, po) :: l ->
+      let (u,nt) = qualified_nterm "tactic" nt in
+      let (etyp, _) = Egrammar.interp_entry_name u nt in
+      etyp :: make_tags l
+  | [] -> []
+
+let declare_pprule = function
+  (* Pretty-printing rules only for Grammar (Tactic Notation) *)
+  | Egrammar.TacticGrammar gl ->
+      let f (s,(s',l),tac) =
+        let pp = (make_tags l, (s',List.map make_terminal_status l)) in
+        Pptactic.declare_extra_tactic_pprule true s pp;
+        Pptactic.declare_extra_tactic_pprule false s pp in
+      List.iter f gl
+  | _ -> ()
+
+let cache_grammar (_,a) =
+  Egrammar.extend_grammar a;
+  declare_pprule a
+
+let subst_grammar (_,subst,a) =
+  Egrammar.subst_all_grammar_command subst a
 
 let (inGrammar, outGrammar) =
   declare_object {(default_object "GRAMMAR") with