From e0380f347d2ebf61b81760a365eea8c84ad3ada4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Oct 2020 17:39:39 +0200
Subject: [attributes] Allow boolean, single-value attributes.

Following discussion in https://github.com/coq/coq/pull/12586 , we
extend the syntax `val=string` to support also arbitrary values.

In particular we support boolean ones, or arbitrary key-pair lists.

This complements the current form `val="string"`, and makes more sense
in general.

Current syntax for the boolean version is `attr=yes` or `attr=no`, but
we could be more liberal if desired.

The general new guideline is that `foo(vals)` is reserved for
the case where `vals` is a list, whereas `foo=val` is for attributes
that allow a unique assignment.

This commit only introduces the support, next commits will migrate
some attributes to this new syntax and deprecate the old versions.
---
 vernac/attributes.mli | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

(limited to 'vernac/attributes.mli')

diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 1969665082..60195fe790 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,20 @@ 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={on,off}]. 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
+   [name(on)] [name(off)] and new attribute syntax, with [on] taken as
+   the key. *)
 
 val qualify_attribute : string -> 'a attribute -> 'a attribute
 (** [qualified_attribute qual att] treats [#[qual(atts)]] like [att]
-- 
cgit v1.2.3


From c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Nov 2020 20:21:36 +0100
Subject: [attributes] Deprecate `attr(true)` syntax in favor of booelan
 attributes.

We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).

We update the documentation, test-suite, and changelog.
---
 vernac/attributes.mli | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac/attributes.mli')

diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 60195fe790..03a14a03ff 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -88,7 +88,7 @@ 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. *)
 
-(** Define boolean attribute [name], of the form [name={on,off}]. The
+(** 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
 
@@ -99,9 +99,8 @@ val deprecated_bool_attribute
   -> 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
-   [name(on)] [name(off)] and new attribute syntax, with [on] taken as
-   the key. *)
+   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]
-- 
cgit v1.2.3