Prevent a symbol from consuming whitespace

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Observe that in the following example, all the whitespace following cat becomes part of that token in the trailing field of SourceInfo.original. I am wondering if there is a way to prevent that, and instead put it in the leading part of 123.

import Lean

declare_syntax_cat aCat
syntax "cat" term : aCat

elab "#parse" a:aCat : command => do
  Lean.logInfo m!"{repr a}"

/-
{ raw := Lean.Syntax.node
           (Lean.SourceInfo.none)
           `aCatCat_
           #[Lean.Syntax.atom
               (Lean.SourceInfo.original "".toSubstring { byteIdx := 136 } "/- -/ ".toSubstring { byteIdx := 139 })
               "cat",
             Lean.Syntax.node
               (Lean.SourceInfo.none)
               `num
               #[Lean.Syntax.atom
                   (Lean.SourceInfo.original "".toSubstring { byteIdx := 145 } "".toSubstring { byteIdx := 148 })
                   "123"]] }
-/
#parse cat/- -/ 123

[Sebastian Ullrich]

What would be the heuristic? docs#Lean.Syntax.updateLeading implements a different heuristic but may be useful as a template

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

How would I use updateLeading, or my own version? It is a function Syntax -> Syntax, but I want to adapt the parser to use it. The parser does not "see" the preceding token, so I don't even know how to access the information from that.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

(As an aside, it looks like updateLeading isn't used anywhere except for testParseModule.)

[Sebastian Ullrich]

Why does it have to happen in the parser?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Uh, where else can it happen? Sorry for asking confused questions; ultimately what I am trying to achieve is to make that one example work, in the sense that the sub-Syntax parsed by term gets the whitespace stored in it, so any suggestion on how to concretely do it would help.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Or are you saying I should take the whole syntax tree for aCat and modify it post-hoc?

[Sebastian Ullrich]

Yes, that was the plan for updateLeading though as you noticed, it isn't used right now because we haven't begun doing any concrete syntax tree transformations