Get syntax range in pattern matching

Stream: lean4

[Patrick Massot]

When matching some syntax I know I can use %$tk to record one piece of syntax that was matched. Is there a way to do that with several consecutive pieces? Or am I meant to create a syntax category for the suggestion I want?

[Sebastian Ullrich]

Do you mean their lexical range? You can put the first and last token in a mkNullNode and get the range of that

[Patrick Massot]

Yes I want to get their lexical range. I don’t know what it means to “put the first and last token in a mkNullNode and get the range of that”.

[Patrick Massot]

And the context of this question is described at #lean4 > Show tactic state and widget in custom calc @ 💬

[Patrick Massot]

I just moved that thread because I just noticed I originally put it in the mathlib4 channel by accident.

[Damiano Testa]

Is something like this what you are looking for?

import Lean

elab tk:group("these" "are" "all" "together") "these" "are" "not" : command => do
  Lean.logInfoAt tk "Underlying them all"
  return

these are all together these are not

[Patrick Massot]

I’m looking for the analogue of that when doing pattern matching.

[Sebastian Ullrich]

mkNullNode #[firstTk, lastTk] is a Syntax spanning the two tokens. It's not a valid syntax to elaborate but likely it works for the widget and withTacticInfoContext, which is responsible for annotating a syntax range with the pre and post state of executing a tactic