feat: introduce suppressInsideQuot

src/Lean/Parser/Basic.lean

@@ -124,12 +124,13 @@ instance : Inhabited InputContext := ⟨{
 }⟩
 
 structure ParserContext extends InputContext :=
-  (prec         : Nat)
-  (env          : Environment)
-  (tokens       : TokenTable)
-  (insideQuot   : Bool := false)
-  (savedPos?    : Option Position := none)
-  (forbiddenTk? : Option Token := none)
+  (prec               : Nat)
+  (env                : Environment)
+  (tokens             : TokenTable)
+  (insideQuot         : Bool := false)
+  (suppressInsideQuot : Bool := false)
+  (savedPos?          : Option Position := none)
+  (forbiddenTk?       : Option Token := none)
 
 structure Error :=
   (unexpected : String := "")
@@ -394,13 +395,22 @@ def checkOutsideQuotFn : ParserFn := fun c s =>
 }
 
 def toggleInsideQuotFn (p : ParserFn) : ParserFn := fun c s =>
-  p { c with insideQuot := !c.insideQuot } s
+  if c.suppressInsideQuot then p c s
+  else p { c with insideQuot := !c.insideQuot } s
 
 @[inline] def toggleInsideQuot (p : Parser) : Parser := {
-  info := epsilonInfo,
+  info := p.info,
   fn   := toggleInsideQuotFn p.fn
 }
 
+def suppressInsideQuotFn (p : ParserFn) : ParserFn := fun c s =>
+  p { c with suppressInsideQuot := true } s
+
+@[inline] def suppressInsideQuot (p : Parser) : Parser := {
+  info := p.info,
+  fn   := suppressInsideQuotFn p.fn
+}
+
 @[inline] def leadingNode (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=
   checkPrec prec >> node n p
 

src/Lean/Parser/Syntax.lean

@@ -64,11 +64,13 @@ def «postfix»  := parser! "postfix"
 def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
 @[builtinCommandParser] def «mixfix»   := parser! mixfixKind >> optPrecedence >> 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! "notation" >> optPrecedence >> many notationItem >> darrow >> termParser
-@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> optKind >> Term.matchAlts
+@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts)
 def parserKind     := parser! ident
 def parserPrio     := parser! numLit
 def parserKindPrio := parser! «try» (ident >> ", ") >> numLit
@@ -83,13 +85,13 @@ def macroTailTactic   : Parser := «try» (" : " >> identEq "tactic") >> darrow
 def macroTailCommand  : Parser := «try» (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
 def macroTailDefault  : Parser := «try» (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
-@[builtinCommandParser] def «macro»       := parser! "macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail
+@[builtinCommandParser] def «macro»       := parser! suppressInsideQuot ("macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail)
 
-@[builtinCommandParser] def «elab_rules» := parser! "elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts
+@[builtinCommandParser] def «elab_rules» := parser! suppressInsideQuot ("elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts)
 def elabHead := macroHead
 def elabArg  := macroArg
 def elabTail := «try» (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> termParser
-@[builtinCommandParser] def «elab»       := parser! "elab " >> optPrecedence >> elabHead >> many elabArg >> elabTail
+@[builtinCommandParser] def «elab»       := parser! suppressInsideQuot ("elab " >> optPrecedence >> elabHead >> many elabArg >> elabTail)
 
 end Command
 

src/Lean/PrettyPrinter/Formatter.lean

@@ -357,8 +357,8 @@ def sepBy.formatter (p pSep : Formatter) : Formatter := do
 @[combinatorFormatter Lean.Parser.setExpected]
 def setExpected.formatter (expected : List String) (p : Formatter) : Formatter := p
 
-@[combinatorFormatter Lean.Parser.toggleInsideQuot]
-def toggleInsideQuot.formatter (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.toggleInsideQuot] def toggleInsideQuot.formatter (p : Formatter) : Formatter := p
+@[combinatorFormatter Lean.Parser.suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p
 
 @[combinatorFormatter Lean.Parser.checkWsBefore] def checkWsBefore.formatter : Formatter := do
   let st ← get

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -439,8 +439,8 @@ def sepBy.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
 @[combinatorParenthesizer Lean.Parser.setExpected]
 def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer := p
 
-@[combinatorParenthesizer Lean.Parser.toggleInsideQuot]
-def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.toggleInsideQuot] def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
+@[combinatorParenthesizer Lean.Parser.suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
 
 @[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()