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/ppvernac.ml | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'vernac/ppvernac.ml')

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 442269ebda..4cee4f7a47 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1331,20 +1331,10 @@ let pr_control_flag (p : control_flag) =
 
 let pr_vernac_control flags = Pp.prlist pr_control_flag flags
 
-let rec pr_vernac_flag (k, v) =
-  let k = keyword k in
-  let open Attributes in
-  match v with
-  | VernacFlagEmpty -> k
-  | VernacFlagLeaf v -> k ++ str " = " ++ qs v
-  | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )"
-and pr_vernac_flags m =
-  prlist_with_sep (fun () -> str ", ") pr_vernac_flag m
-
 let pr_vernac_attributes =
   function
   | [] -> mt ()
-  | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
+  | flags ->  str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut ()
 
 let pr_vernac ({v = {control; attrs; expr}} as v) =
   tag_vernac v
-- 
cgit v1.2.3