From c6ab0b4d2cb604c91d0faab613b999acbfa8317d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Dec 2020 07:00:06 -0800 Subject: [PATCH] feat: allow `local` modifier at `infix`, `notation`, and `syntax` commands --- src/Lean/Parser/Syntax.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 62d892f86b..5872ba0ae6 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -44,25 +44,28 @@ namespace Command def optPrio := optional ("[" >> numLit >> "]") +def «scoped» := parser! "scoped " +def «local» := parser! "local " +def attrKind := optional («scoped» <|> «local») def «prefix» := parser! "prefix" def «infix» := parser! "infix" def «infixl» := parser! "infixl" def «infixr» := parser! "infixr" def «postfix» := parser! "postfix" def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix» -@[builtinCommandParser] def «mixfix» := parser! optional "scoped " >> mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser +@[builtinCommandParser] def «mixfix» := parser! attrKind >> mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser -- NOTE: We use `suppressInsideQuot` in the following parsers because quotations inside them are evaluated in the same stage and -- thus should be ignored when we use `checkInsideQuot` to prepare the next stage for a builtin syntax change def identPrec := parser! ident >> optPrecedence def optKind : Parser := optional ("[" >> ident >> "]") def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec) -@[builtinCommandParser] def «notation» := parser! optional "scoped " >> "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser +@[builtinCommandParser] def «notation» := parser! attrKind >> "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser @[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts) def parserKind := parser! ident def parserPrio := parser! numLit def parserKindPrio := parser! atomic (ident >> ", ") >> numLit def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|> parserPrio) >> "]") -@[builtinCommandParser] def «syntax» := parser! optional "scoped " >> "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident +@[builtinCommandParser] def «syntax» := parser! attrKind >> "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident @[builtinCommandParser] def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser @[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec