From 8520cc7a02bedf4f4820ef198550f7cfa2a6454c Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 31 May 2018 08:57:47 +0000
Subject: [vernac] Concrete syntax for attributes

---
 vernac/ppvernac.ml | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'vernac/ppvernac.ml')

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5fbe1f4e4..b49fb011b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -153,8 +153,6 @@ open Pputils
       | SearchAbout sl ->
          keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
-  let pr_locality local = if local then keyword "Local" else keyword "Global"
-
   let pr_option_ref_value = function
     | QualidRefValue id -> pr_qualid id
     | StringRefValue s -> qs s
@@ -1195,21 +1193,24 @@ open Pputils
       | VernacEndSubproof ->
         return (str "}")
 
-let pr_vernac_flag =
+let pr_vernac_flag f =
+  keyword (match f with
+  | VernacPolymorphic true -> "polymorphic"
+  | VernacPolymorphic false -> "monomorphic"
+  | VernacProgram -> "program"
+  | VernacLocal true -> "local"
+  | VernacLocal false -> "global"
+  )
+
+let pr_vernac_flag_list =
   function
-  | VernacPolymorphic true -> keyword "Polymorphic"
-  | VernacPolymorphic false -> keyword "Monomorphic"
-  | VernacProgram -> keyword "Program"
-  | VernacLocal local -> pr_locality local
+  | [] -> mt ()
+  | flags ->  str "#[" ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag flags ++ str "]" ++ cut ()
 
   let rec pr_vernac_control v =
     let return = tag_vernac v in
     match v with
-    | VernacExpr (f, v') ->
-      List.fold_right
-        (fun f a -> pr_vernac_flag f ++ spc() ++ a)
-        f
-        (pr_vernac_expr v' ++ sep_end v')
+    | VernacExpr (f, v') -> pr_vernac_flag_list f ++ pr_vernac_expr v' ++ sep_end v'
     | VernacTime (_,{v}) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
     | VernacRedirect (s, {v}) ->
-- 
cgit v1.2.3