feat: run single non-category quotation under interpreter as well

src/Lean/Parser/Basic.lean

@@ -1715,6 +1715,14 @@ constant parserOfStackFn (offset : Nat) : ParserFn
 def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser :=
   { fn := fun c s => parserOfStackFn offset { c with prec := prec } s }
 
+/-- Run `declName` if possible and inside a quotation, or else `p`. The `ParserInfo` will always be taken from `p`. -/
+def evalInsideQuot (declName : Name) (p : Parser) : Parser := { p with
+  fn := fun c s =>
+    if c.insideQuot && c.env.contains declName then
+      evalParserConst declName c s
+    else
+      p.fn c s }
+
 private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
   if s.stackSize == iniSz + 1 then s
   else s.mkNode nullKind iniSz -- throw error instead?

src/Lean/Parser/Extension.lean

@@ -144,13 +144,9 @@ private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit
   | Except.error msg     => throw (IO.userError s!"invalid builtin parser '{declName}', {msg}")
 
 def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
-  let fn : ParserFn := fun c s =>
-    if c.insideQuot && c.env.contains declName then
-      evalParserConst declName c s
-    else
-      p.fn c s
+  let p := evalInsideQuot declName p
   let categories ← builtinParserCategoriesRef.get
-  let categories ← IO.ofExcept $ addParser categories catName declName leading { p with fn := fn } prio
+  let categories ← IO.ofExcept $ addParser categories catName declName leading p prio
   builtinParserCategoriesRef.set categories
   builtinSyntaxNodeKindSetRef.modify p.info.collectKinds
   updateBuiltinTokens p.info declName

src/Lean/Parser/Term.lean

@@ -197,7 +197,8 @@ def isIdent (stx : Syntax) : Bool :=
 
 @[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
 
-@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
+-- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly
+@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot (evalInsideQuot ``funBinder funBinder) >> ")"
 
 @[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"

src/Lean/PrettyPrinter/Formatter.lean

@@ -404,6 +404,7 @@ def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :
 
 @[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.evalInsideQuot] def evalInsideQuot.formatter (declName : Name) (p : Formatter) : Formatter := p
 
 @[combinatorFormatter Lean.Parser.checkWsBefore] def checkWsBefore.formatter : Formatter := do
   let st ← get

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -464,6 +464,7 @@ def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Par
 
 @[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.evalInsideQuot] def evalInsideQuot.parenthesizer (declName : Name) (p : Parenthesizer) : Parenthesizer := p
 
 @[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()