From 216d34e178ada5d09c41eba19ed7ead6baceb642 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Dec 2020 13:13:58 -0800 Subject: [PATCH] feat: add `prio` parser category --- src/Lean/Parser/Syntax.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 8efaeedbef..a260cd3922 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -17,9 +17,16 @@ builtin_initialize registerBuiltinParserAttribute `builtinPrecParser `prec (leadingIdentAsSymbol := true) registerBuiltinDynamicParserAttribute `precParser `prec +builtin_initialize + registerBuiltinParserAttribute `builtinPrioParser `prio (leadingIdentAsSymbol := true) + registerBuiltinDynamicParserAttribute `prioParser `prio + @[inline] def precedenceParser (rbp : Nat := 0) : Parser := categoryParser `prec rbp +@[inline] def priorityParser (rbp : Nat := 0) : Parser := + categoryParser `prio rbp + @[inline] def syntaxParser (rbp : Nat := 0) : Parser := categoryParser `stx rbp @@ -45,6 +52,7 @@ namespace Term @[builtinTermParser] def stx.quot : Parser := parser! "`(stx|" >> toggleInsideQuot syntaxParser >> ")" @[builtinTermParser] def prec.quot : Parser := parser! "`(prec|" >> toggleInsideQuot precedenceParser >> ")" +@[builtinTermParser] def prio.quot : Parser := parser! "`(prio|" >> toggleInsideQuot priorityParser >> ")" end Term