Confusing syntax match

Stream: lean4

[Wojciech Nawrocki]

I am a bit baffled by the following error. Screenshot instead of text since the error span is on the exact expected symbol.

[Sebastian Ullrich]

@Wojciech Nawrocki Ah, that's unfortunate. Tokens are registered only when a surrounding parser is hooked into a parser category. So at this point, blocking is still an identifier.

[Wojciech Nawrocki]

@Sebastian Ullrich what does it mean for a surrounding parser to be hooked into a parser category? The #xy is that I would like to use this in a tactic like

syntax "specialize_def" ident "[" term,* "]" optional(blockingConsts) : tactic

Should I invent a fake syntax category or ..?

[Sebastian Ullrich]

At that point it is hooked into the tactic category :) . You just need to move that line up above foo

[Wojciech Nawrocki]

Ah I see, but it doesn't work with elab:

syntax blockingConsts := "blocking" "[" ident,* "]"
elab "specialize_def" i:ident "[" ts:term,* "]" block?:optional(blockingConsts) : tactic => do
  /- expected 'blocking' -/
  if let `(blockingConsts|blocking [ $is:ident,* ]) := block? then
    sorry
  sorry

[Sebastian Ullrich]

Ahh, yeah, the generated parser is registered only after the entire command has been parsed