diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 816d1acdf7..f5459abb5e 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -429,11 +429,11 @@ def elabSyntax (stx : Syntax) : CommandElabM Name := do discard <| elabSyntax stx @[builtin_command_elab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do - let `($[$doc?:docComment]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax + let `($[$doc?:docComment]? $[$vis?:visibility]? syntax $declName:ident := $[$ps:stx]*) ← pure stx | throwUnsupportedSyntax -- TODO: nonatomic names let (val, _) ← runTermElabM fun _ => Term.toParserDescr (mkNullNode ps) Name.anonymous let stxNodeKind := (← getCurrNamespace) ++ declName.getId - let stx' ← `($[$doc?:docComment]? meta def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val) + let stx' ← `($[$doc?:docComment]? $[$vis?:visibility]? meta def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val) withMacroExpansion stx stx' <| elabCommand stx' def checkRuleKind (given expected : SyntaxNodeKind) : Bool := diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index a019237788..ed96795b8d 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -87,7 +87,7 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" decl_name optional docComment >> optional Term.«attributes» >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (ppSpace >> syntaxParser argPrec) >> " : " >> ident @[builtin_command_parser] def syntaxAbbrev := leading_parser - optional docComment >> "syntax " >> ident >> " := " >> many1 syntaxParser + optional docComment >> optional visibility >> "syntax " >> ident >> " := " >> many1 syntaxParser def catBehaviorBoth := leading_parser nonReservedSymbol "both" def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol" def catBehavior := optional (" (" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")