From 767816eece27e6bb8cba0bbf122507bd2a3b77a1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Nov 2017 22:54:24 +0100 Subject: Using a specific function to register vernac printers. --- API/API.mli | 2 ++ dev/doc/changes.md | 7 +++++++ grammar/argextend.mlp | 7 +------ plugins/funind/g_indfun.ml4 | 3 +-- plugins/ltac/g_obligations.ml4 | 4 +--- plugins/ltac/g_rewrite.ml4 | 3 +-- plugins/ltac/pptactic.ml | 4 ++++ plugins/ltac/pptactic.mli | 4 ++++ printing/genprint.ml | 6 ++++++ printing/genprint.mli | 2 ++ 10 files changed, 29 insertions(+), 13 deletions(-) diff --git a/API/API.mli b/API/API.mli index e20793077..608bd43cd 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4977,6 +4977,8 @@ sig val generic_top_print : Genarg.tlevel Genarg.generic_argument printer val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top printer -> unit + val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> + 'raw printer -> unit end module Pputils : diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6ade6576f..b1ebec44e 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -38,6 +38,13 @@ Some tactics and related functions now support static configurability, e.g.: - if None, tells to behave as told with the flag Keep Proof Equalities - if Some b, tells to keep proof equalities iff b is true +Declaration of printers for arguments used only in vernac command + +- It should now use "declare_extra_vernac_genarg_pprule" rather than + "declare_extra_genarg_pprule", otherwise, a failure at runtime might + happen. An alternative is to register the corresponding argument as + a value, using "Geninterp.register_val0 wit None". + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 12b7b171b..9742a002d 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -186,12 +186,7 @@ let declare_vernac_argument loc s pr cl = value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; make_extend loc s cl wit; - <:str_item< do { - Pptactic.declare_extra_genarg_pprule $wit$ - $pr_rules$ - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.")) - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer.")) } - >> ] + <:str_item< Pptactic.declare_extra_vernac_genarg_pprule $wit$ $pr_rules$ >> ] open Pcaml diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 62ecaa552..829556a71 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -144,8 +144,7 @@ END let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - let printer _ _ _ _ = str "" in - Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 1a2d89586..fea9e837b 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -155,6 +155,4 @@ let () = | None -> mt () | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy + Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c22e68323..b148d962e 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -195,8 +195,7 @@ let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wi let () = let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in - let printer _ _ _ _ = Pp.str "" in - Pptactic.declare_extra_genarg_pprule wit_binders raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer open Pcoq diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 2c46b7624..00ce94f6c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1180,6 +1180,10 @@ let declare_extra_genarg_pprule wit in Genprint.register_print0 wit f g h +let declare_extra_vernac_genarg_pprule wit f = + let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + Genprint.register_vernac_print0 wit f + (** Registering *) let run_delayed c = c (Global.env ()) Evd.empty diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 058b20569..b47f07a45 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -46,6 +46,10 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_vernac_genarg_pprule : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer -> unit + type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { diff --git a/printing/genprint.ml b/printing/genprint.ml index 543b05024..b20ea0b62 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -39,6 +39,12 @@ let register_print0 wit raw glb top = let printer = { raw; glb; top; } in Print.register0 wit printer +let register_vernac_print0 wit raw = + let glb _ = CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.") in + let top _ = CErrors.anomaly (Pp.str "vernac argument needs not wit printer.") in + let printer = { raw; glb; top; } in + Print.register0 wit printer + let raw_print wit v = (Print.obj wit).raw v let glb_print wit v = (Print.obj wit).glb v let top_print wit v = (Print.obj wit).top v diff --git a/printing/genprint.mli b/printing/genprint.mli index 130a89c92..76d80f3b5 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -27,3 +27,5 @@ val generic_top_print : tlevel generic_argument printer val register_print0 : ('raw, 'glb, 'top) genarg_type -> 'raw printer -> 'glb printer -> 'top printer -> unit +val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> + 'raw printer -> unit -- cgit v1.2.3