diff options
Diffstat (limited to 'vernac/attributes.mli')
| -rw-r--r-- | vernac/attributes.mli | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 1969665082..03a14a03ff 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -9,13 +9,19 @@ (************************************************************************) (** The type of parsing attribute data *) +type vernac_flag_type = + | FlagIdent of string + | FlagString of string + type vernac_flags = vernac_flag list and vernac_flag = string * vernac_flag_value and vernac_flag_value = | VernacFlagEmpty - | VernacFlagLeaf of string + | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags +val pr_vernac_flag : vernac_flag -> Pp.t + type +'a attribute (** The type of attributes. When parsing attributes if an ['a attribute] is present then an ['a] value will be produced. @@ -82,10 +88,19 @@ val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute (** Make an attribute from a list of key parsers together with their associated key. *) -val bool_attribute : name:string -> on:string -> off:string -> bool option attribute -(** Define boolean attribute [name] with value [true] when [on] is - provided and [false] when [off] is provided. The attribute may only - be set once for a command. *) +(** Define boolean attribute [name], of the form [name={yes,no}]. The + attribute may only be set once for a command. *) +val bool_attribute : name:string -> bool option attribute + +val deprecated_bool_attribute + : name:string + -> on:string + -> off:string + -> bool option attribute +(** Define boolean attribute [name] with will be set when [on] is + provided and unset when [off] is provided. The attribute may only + be set once for a command; this attribute both accepts the old [on] + [off] syntax and new attribute syntax [on=yes] [on=no] *) val qualify_attribute : string -> 'a attribute -> 'a attribute (** [qualified_attribute qual att] treats [#[qual(atts)]] like [att] |