[vernac] Concrete syntax for attributes

2 files changed, 31 insertions, 13 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3a01ce6df..bffdaa0b1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -79,9 +79,26 @@ GRAMMAR EXTEND Gram
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) }
       | IDENT "Timeout"; n = natural; v = vernac_control -> { VernacTimeout(n,v) }
       | IDENT "Fail"; v = vernac_control -> { VernacFail v }
-      | v = vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+      | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
     ]
   ;
+  decorated_vernac:
+  [[ a = attributes ; fv = vernac -> let (f, v) = fv in (List.append a f, v)
+  | fv = vernac -> fv
+  ]]
+  ;
+  attributes: [[ "#[" ; a = LIST1 attribute SEP "," ; "]" -> a ]]
+  ;
+  attribute:
+  [[
+    IDENT "polymorphic" -> VernacPolymorphic true
+  | IDENT "monomorphic" -> VernacPolymorphic false
+  | IDENT "program" -> VernacProgram
+  | IDENT "local" -> VernacLocal true
+  | IDENT "global" -> VernacLocal false
+  | IDENT "coercion" -> VernacCoercion
+  ]]
+  ;
   vernac:
     [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) }
       | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) }
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}) ->