Antiquotes in block category do not work

[eric-wieser]

Minimized to be verso-free:

import Lean

open Lean.Parser (rawIdent)

declare_syntax_cat arg_val
syntax (name:=arg_str) str : arg_val

declare_syntax_cat argument
syntax (name:=anon) arg_val : argument
syntax (name:=named) ident ":=" arg_val : argument

declare_syntax_cat inline

declare_syntax_cat block
syntax (name:=directive) "directive{" rawIdent argument* "}" "[" block* "]": block

syntax (name:=header) inline* : block

example : Lean.TSyntax `block → Bool :=
  fun
  | `(block| directive{foo $args*}[$blocks]) => true
  | _ => false

which fails with "invalid 'many' parser combinator application, parser did not consume anything".

Changing

-syntax (name:=header) inline* : block
+syntax (name:=header) inline+ : block

makes the problem goes away.

[david-christiansen]

Thanks for a great bug report!