diff options
| -rw-r--r-- | vernac/g_vernac.mlg | 19 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 25 |
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}) -> |