Allowing to extend the Print Grammar command generically.

We also move the Ltac-specific grammar to its folder.

2 files changed, 23 insertions, 10 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cd244bf63..bbec5b72d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -46,12 +46,30 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 let entry_buf = Buffer.create 64
 
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammars : any_entry list String.Map.t ref = ref String.Map.empty
+
+let register_grammar name grams =
+  grammars := String.Map.add name grams !grammars
+
 let pr_entry e =
   let () = Buffer.clear entry_buf in
   let ft = Format.formatter_of_buffer entry_buf in
   let () = Gram.entry_print ft e in
   str (Buffer.contents entry_buf)
 
+let pr_registered_grammar name =
+  let gram = try Some (String.Map.find name !grammars) with Not_found -> None in
+  match gram with
+  | None -> error "Unknown or unprintable grammar entry."
+  | Some entries ->
+    let pr_one (AnyEntry e) =
+      str "Entry " ++ str (Gram.Entry.name e) ++ str " is" ++ fnl () ++
+      pr_entry e
+    in
+    prlist pr_one entries
+
 let pr_grammar = function
   | "constr" | "operconstr" | "binder_constr" ->
       str "Entry constr is" ++ fnl () ++
@@ -64,15 +82,6 @@ let pr_grammar = function
       pr_entry Pcoq.Constr.operconstr
   | "pattern" ->
       pr_entry Pcoq.Constr.pattern
-  | "tactic" ->
-      str "Entry tactic_expr is" ++ fnl () ++
-      pr_entry Pcoq.Tactic.tactic_expr ++
-      str "Entry binder_tactic is" ++ fnl () ++
-      pr_entry Pcoq.Tactic.binder_tactic ++
-      str "Entry simple_tactic is" ++ fnl () ++
-      pr_entry Pcoq.Tactic.simple_tactic ++
-      str "Entry tactic_arg is" ++ fnl () ++
-      pr_entry Pcoq.Tactic.tactic_arg
   | "vernac" ->
       str "Entry vernac is" ++ fnl () ++
       pr_entry Pcoq.Vernac_.vernac ++
@@ -84,7 +93,7 @@ let pr_grammar = function
       pr_entry Pcoq.Vernac_.gallina ++
       str "Entry gallina_ext is" ++ fnl () ++
       pr_entry Pcoq.Vernac_.gallina_ext
-  | _ -> error "Unknown or unprintable grammar entry."
+  | name -> pr_registered_grammar name
 
 (**********************************************************************)
 (* Parse a format (every terminal starting with a letter or a single
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f978ec352..57c120402 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -54,6 +54,10 @@ val add_syntactic_definition : Id.t -> Id.t list * constr_expr ->
 
 val pr_grammar : string -> Pp.std_ppcmds
 
+type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
+
+val register_grammar : string -> any_entry list -> unit
+
 val check_infix_modifiers : syntax_modifier list -> unit
 
 val with_syntax_protection : ('a -> 'b) -> 'a -> 'b