diff options
Diffstat (limited to 'parsing/argextend.ml4')
| -rw-r--r-- | parsing/argextend.ml4 | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 57e88133..bd6be424 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: argextend.ml4 10122 2007-09-15 10:35:59Z letouzey $ *) +(* $Id: argextend.ml4 11622 2008-11-23 08:45:56Z herbelin $ *) open Genarg open Q_util @@ -25,7 +25,7 @@ let rec make_rawwit loc = function | StringArgType -> <:expr< Genarg.rawwit_string >> | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >> - | IdentArgType -> <:expr< Genarg.rawwit_ident >> + | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.rawwit_var >> | RefArgType -> <:expr< Genarg.rawwit_ref >> | SortArgType -> <:expr< Genarg.rawwit_sort >> @@ -50,7 +50,7 @@ let rec make_globwit loc = function | StringArgType -> <:expr< Genarg.globwit_string >> | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >> - | IdentArgType -> <:expr< Genarg.globwit_ident >> + | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.globwit_var >> | RefArgType -> <:expr< Genarg.globwit_ref >> | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >> @@ -75,7 +75,7 @@ let rec make_wit loc = function | StringArgType -> <:expr< Genarg.wit_string >> | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> - | IdentArgType -> <:expr< Genarg.wit_ident >> + | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.wit_var >> | RefArgType -> <:expr< Genarg.wit_ref >> | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> @@ -163,16 +163,27 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = end >> -let declare_vernac_argument loc s cl = +let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in + let wit = <:expr< $lid:"wit_"^s$ >> in let rawwit = <:expr< $lid:"rawwit_"^s$ >> in + let globwit = <:expr< $lid:"globwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in + let pr_rules = match pr with + | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> + | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in <:str_item< declare - value $lid:"rawwit_"^s$ = let (_,_,x) = Genarg.create_arg $se$ in x; + value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel), + ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel), + $lid:"rawwit_"^s$) = Genarg.create_arg $se$; value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; + Pptactic.declare_extra_genarg_pprule + ($rawwit$, $pr_rules$) + ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer") + ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer"); end >> @@ -202,11 +213,12 @@ EXTEND failwith "Argument entry names must be lowercase"; declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; + pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> if String.capitalize s = s then failwith "Argument entry names must be lowercase"; - declare_vernac_argument loc s l ] ] + declare_vernac_argument loc s pr l ] ] ; argtype: [ "2" |