diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 953ddc79ef..e2720bdcd9 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -231,9 +231,16 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d @[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do let catName := stx[1].getId + let catBehavior := + if stx[2].isNone then + Parser.LeadingIdentBehavior.default + else if stx[2][3].getKind == ``Parser.Command.catBehaviorBoth then + Parser.LeadingIdentBehavior.both + else + Parser.LeadingIdentBehavior.symbol let attrName := catName.appendAfter "Parser" let env ← getEnv - let env ← liftIO $ Parser.registerParserCategory env attrName catName + let env ← Parser.registerParserCategory env attrName catName catBehavior setEnv env declareSyntaxCatQuotParser catName diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 47ee936c8a..fdc301496a 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1593,8 +1593,7 @@ inductive LeadingIdentBehavior where | default | symbol | both - deriving Inhabited, BEq - + deriving Inhabited, BEq, Repr /-- Each parser category is implemented using a Pratt's parser. diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 50eeebf5f1..1d8750f9e2 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -71,7 +71,10 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Par @[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser optional docComment >> Term.attrKind >> "macro_rules" >> optKind >> Term.matchAlts) @[builtinCommandParser] def «syntax» := leading_parser optional docComment >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident @[builtinCommandParser] def syntaxAbbrev := leading_parser "syntax " >> ident >> " := " >> many1 syntaxParser -@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident +def catBehaviorBoth := leading_parser nonReservedSymbol "both" +def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol" +def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")") +@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident >> catBehavior def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> termParser def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1