Taking into account the original grammar rule to print generic

arguments of vernac extensions, so that in list with a separator, the
separator is printed.

3 files changed, 58 insertions, 11 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f584521765..c3c4009ca1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -70,6 +70,17 @@ let declare_extra_genarg_pprule wit f g h =
   let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
   genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule
 
+let find_extra_genarg_pprule wit =
+  let s = match wit with
+    | ExtraArg s -> ArgT.repr s
+    | _ -> error
+      "Can declare a pretty-printing rule only for extra argument types."
+  in
+  let (f,g,h) = String.Map.find s !genarg_pprule in
+  (fun prc prlc prtac x -> f prc prlc prtac (in_gen (rawwit wit) x)),
+  (fun prc prlc prtac x -> g prc prlc prtac (in_gen (glbwit wit) x)),
+  (fun prc prlc prtac x -> h prc prlc prtac (in_gen (topwit wit) x))
+
 module Make
   (Ppconstr : Ppconstrsig.Pp)
   (Taggers : sig
@@ -298,7 +309,6 @@ module Make
         try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
         with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
 
-
   let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
     match wit with
       | ListArg wit ->
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 1608cae751..270f709b72 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -41,6 +41,12 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
+val find_extra_genarg_pprule :
+  ('a, 'b, 'c) genarg_type ->
+  'a raw_extra_genarg_printer *
+  'b glob_extra_genarg_printer *
+  'c extra_genarg_printer
+
 type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index efdaa366bb..fb9dca255c 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -21,7 +21,7 @@ open Decl_kinds
 
 module Make
   (Ppconstr : Ppconstrsig.Pp)
-  (Pptactic : Pptacticsig.Pp)
+  (Pptacticsig : Pptacticsig.Pp)
   (Taggers  : sig
     val tag_keyword : std_ppcmds -> std_ppcmds
     val tag_vernac  : vernac_expr -> std_ppcmds -> std_ppcmds
@@ -30,7 +30,7 @@ module Make
 
   open Taggers
   open Ppconstr
-  open Pptactic
+  open Pptacticsig
 
   let keyword s = tag_keyword (str s)
 
@@ -81,11 +81,39 @@ module Make
     | VernacEndSubproof -> str""
     | _ -> str"."
 
-  let pr_gen t = pr_raw_generic (Global.env ()) t
-
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
+  open Genarg
+
+  type 'c entry_name = EntryName : ('c, 'a) Extend.symbol -> 'c entry_name
+
+  let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
+
+  let rec pr_gen = function
+    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist1 e) ->
+        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
+        hov_if_not_empty 0 (pr_sequence map x)
+    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist0 e) ->
+        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
+        hov_if_not_empty 0 (pr_sequence map x)
+    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist1sep (e,sep)) ->
+        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
+        hov_if_not_empty 0 (prlist_with_sep (fun () -> spc() ++ str sep ++ spc()) map x)
+    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist0sep (e,sep)) ->
+        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
+        hov_if_not_empty 0 (prlist_with_sep (fun () -> spc() ++ str sep ++ spc()) map x)
+    | GenArg (Rawwit (OptArg wit), x), EntryName (Aopt e) ->
+        let ans = match x with
+          | None -> mt ()
+          | Some x -> pr_gen (GenArg (rawwit wit, x), EntryName e) in
+        hov_if_not_empty 0 ans
+    | GenArg (Rawwit (PairArg (wit1, wit2)), _), _ -> error "Pair of entries not implemented."
+    | GenArg (Rawwit (ExtraArg s as wit), x), e ->
+        (try pi1 (Pptactic.find_extra_genarg_pprule wit) pr_constr_expr pr_lconstr_expr (fun _ -> pr_raw_tactic) x
+        with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x))
+    | _, _ -> assert false
+
   let pr_set_entry_type = function
     | ETName -> str"ident"
     | ETReference -> str"global"
@@ -1201,20 +1229,23 @@ module Make
         return (str "}")
 
   and pr_extend s cl =
-    let pr_arg a =
+    let pr_based_on_grammar a =
       try pr_gen a
       with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
+    let pr_based_on_structure a =
+      try Pptactic.pr_raw_generic (Global.env ()) a
+      with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
     try
       let rl = Egramml.get_extend_vernac_rule s in
-      let rec aux rl cl =
+      let rec aux sep rl cl =
         match rl, cl with
-        | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
-        | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+        | Egramml.GramNonTerminal (_,_,e) :: rl, (GenArg (wit,x)) :: cl -> pr_based_on_grammar (GenArg (wit,x),EntryName e) :: aux sep rl cl
+        | Egramml.GramTerminal s :: rl, cl -> sep() ++ str s :: aux spc rl cl
         | [], [] -> []
         | _ -> assert false in
-      hov 1 (pr_sequence (fun x -> x) (aux rl cl))
+      hov 1 (pr_sequence (fun x -> x) (aux mt rl cl))
     with Not_found ->
-      hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+      hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_based_on_structure cl ++ str ")")
 
   let pr_vernac v =
     try pr_vernac_body v ++ sep_end v