Naming a subexpression of a Syntax match

Stream: lean4

[Eric Wieser]

I have a macro of the form

macro_rules
  | `(!![$[$[$rows],*];*]) => do

which matches things like !![a, b; c d].

How can I obtain a Syntax object corresponding to the entire a, b row, so that I can use it with docs4#Macro.throwErrorAt ?

[Sebastian Ullrich]

If it's just about the error range, we often stick the beginning and end into mkNullNode for that purpose

[Eric Wieser]

Is there any way to obtain the Syntax nodes corresponding to the , and ; tokens?

[Eric Wieser]

Or in general, to capture position information in a syntax match, in order to pass it to mkNullNode later

[Mario Carneiro]

not using the fancy syntax

[Mario Carneiro]

I would love to have some kind of $tk@ syntax for capturing tokens

[Eric Wieser]

mkNullNode was good enough in the end

[Eric Wieser]

(context is !4#3427)