Merge PR #10061: Print custom grammar entries

Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: jashug

6 files changed, 13 insertions, 3 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 59d2a66259..94d4ed80d1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1003,6 +1003,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Grammar"; ent = IDENT ->
           (* This should be in "syntax" section but is here for factorization*)
 	  { PrintGrammar ent }
+      | IDENT "Custom"; IDENT "Grammar"; ent = IDENT ->
+          (* Should also be in "syntax" section *)
+          { PrintCustomGrammar ent }
       | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir }
       | IDENT "Modules" ->
           { user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 843296d24e..50914959dc 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -50,10 +50,10 @@ let pr_entry e =
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
-  let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in
+  let gram = Pcoq.find_grammars_by_name name in
   match gram with
-  | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
-  | Some entries ->
+  | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.")
+  | entries ->
     let pr_one (Pcoq.AnyEntry e) =
       str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
       pr_entry e
@@ -85,6 +85,8 @@ let pr_grammar = function
       pr_entry Pvernac.Vernac_.gallina_ext
   | name -> pr_registered_grammar name
 
+let pr_custom_grammar name = pr_registered_grammar ("constr:"^name)
+
 (**********************************************************************)
 (* Parse a format (every terminal starting with a letter or a single
    quote (except a single quote alone) must be quoted) *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 38dbdf7e41..6435df23c7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
 (** Print the Camlp5 state of a grammar *)
 
 val pr_grammar : string -> Pp.t
+val pr_custom_grammar : string -> Pp.t
 
 val check_infix_modifiers : syntax_modifier list -> unit
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 889dbafabd..f2332bab8b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -476,6 +476,8 @@ open Pputils
       keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
     | PrintGrammar ent ->
       keyword "Print Grammar" ++ spc() ++ str ent
+    | PrintCustomGrammar ent ->
+      keyword "Print Custom Grammar" ++ spc() ++ str ent
     | PrintLoadPath dir ->
       keyword "Print LoadPath" ++ pr_opt DirPath.print dir
     | PrintModules ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 279d4f0935..c7795602aa 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1885,6 +1885,7 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts =
   | PrintSectionContext qid -> print_sec_context_typ env sigma qid
   | PrintInspect n -> inspect env sigma n
   | PrintGrammar ent -> Metasyntax.pr_grammar ent
+  | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent
   | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
   | PrintModules -> print_modules ()
   | PrintModule qid -> print_module qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 34a9b9394a..6a51fdfe59 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -29,6 +29,7 @@ type printable =
   | PrintSectionContext of qualid
   | PrintInspect of int
   | PrintGrammar of string
+  | PrintCustomGrammar of string
   | PrintLoadPath of DirPath.t option
   | PrintModules
   | PrintModule of qualid