fix: bound syntax kind at v:(ppSpace ident) etc.

src/Lean/Elab/MacroArgUtil.lean

@@ -45,8 +45,7 @@ where
   mkSplicePat (kind : SyntaxNodeKind) (stx : TSyntax `stx) (id : Term) (suffix : String) : CommandElabM Term :=
     return ⟨mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]⟩
   mkAntiquotNode : TSyntax `stx → Term → CommandElabM Term
-    | `(stx| ($stx)), term => mkAntiquotNode stx term
-    | `(stx| $id:ident$[:$p:prec]?), term => do
+    | `(stx| $id:ident$[:$_]?), term => do
       let kind ← match (← Elab.Term.resolveParserName id) with
         | [(`Lean.Parser.ident, _)] => pure identKind
         | [(`Lean.Parser.Term.ident, _)] => pure identKind
@@ -63,7 +62,18 @@ where
           else
             throwError "unknown parser declaration/category/alias '{id}'"
       pure ⟨Syntax.mkAntiquotNode kind term⟩
-    | stx, term =>
+    | stx, term => do
+      -- can't match against `` `(stx| ($stxs*)) `` as `*` is interpreted as the `stx` operator
+      if stx.raw.isOfKind ``Parser.Syntax.paren then
+        -- translate argument `v:(p1 ... pn)` where all but one `pi` produce zero nodes to
+        -- `v:pi` using that single `pi`
+        let nonNullaryNodes ← stx.raw[1].getArgs.filterM fun
+          | `(stx| $id:ident$[:$_]?) | `(stx| $id:ident($_)) => do
+            let info ← Parser.getParserAliasInfo id.getId
+            return info.stackSz? != some 0
+          | _ => return true
+        if let #[stx] := nonNullaryNodes then
+          return (← mkAntiquotNode ⟨stx⟩ term)
       pure ⟨Syntax.mkAntiquotNode Name.anonymous term (isPseudoKind := true)⟩
 
 end Lean.Elab.Command

src/Lean/Parser.lean

@@ -19,17 +19,17 @@ open Lean.PrettyPrinter.Parenthesizer
 open Lean.PrettyPrinter.Formatter
 
 builtin_initialize
-  register_parser_alias "ws" checkWsBefore { stackSz? := none }
-  register_parser_alias "noWs" checkNoWsBefore { stackSz? := none }
-  register_parser_alias "linebreak" checkLinebreakBefore { stackSz? := none }
+  register_parser_alias "ws" checkWsBefore { stackSz? := some 0 }
+  register_parser_alias "noWs" checkNoWsBefore { stackSz? := some 0 }
+  register_parser_alias "linebreak" checkLinebreakBefore { stackSz? := some 0 }
   register_parser_alias (kind := numLitKind) "num" numLit
   register_parser_alias (kind := strLitKind) "str" strLit
   register_parser_alias (kind := charLitKind) "char" charLit
   register_parser_alias (kind := nameLitKind) "name" nameLit
   register_parser_alias (kind := scientificLitKind) "scientific" scientificLit
   register_parser_alias (kind := identKind) "ident" ident
-  register_parser_alias "colGt" checkColGt { stackSz? := none }
-  register_parser_alias "colGe" checkColGe { stackSz? := none }
+  register_parser_alias "colGt" checkColGt { stackSz? := some 0 }
+  register_parser_alias "colGe" checkColGe { stackSz? := some 0 }
   register_parser_alias lookahead { stackSz? := some 0 }
   register_parser_alias atomic { stackSz? := none }
   register_parser_alias many

src/Lean/Parser/Extra.lean

@@ -181,17 +181,17 @@ macro_rules
 
 builtin_initialize
   register_parser_alias group { autoGroupArgs := false }
-  register_parser_alias ppHardSpace { stackSz? := none }
-  register_parser_alias ppSpace { stackSz? := none }
-  register_parser_alias ppLine { stackSz? := none }
+  register_parser_alias ppHardSpace { stackSz? := some 0 }
+  register_parser_alias ppSpace { stackSz? := some 0 }
+  register_parser_alias ppLine { stackSz? := some 0 }
   register_parser_alias ppGroup { stackSz? := none }
   register_parser_alias ppRealGroup { stackSz? := none }
   register_parser_alias ppRealFill { stackSz? := none }
   register_parser_alias ppIndent { stackSz? := none }
   register_parser_alias ppDedent { stackSz? := none }
-  register_parser_alias ppAllowUngrouped { stackSz? := none }
   register_parser_alias ppDedentIfGrouped { stackSz? := none }
-  register_parser_alias ppHardLineUnlessUngrouped { stackSz? := none }
+  register_parser_alias ppAllowUngrouped { stackSz? := some 0 }
+  register_parser_alias ppHardLineUnlessUngrouped { stackSz? := some 0 }
 
 end Parser
 

tests/lean/run/1274.lean

@@ -0,0 +1,2 @@
+macro "👉" t:(ppSpace ident) : term => `($t)
+macro "👈" t:(lookahead(term) ident ppSpace) : term => `($t)