Does Lean have a token specification?

Stream: Is there code for X?

[Read-Eval-Loop]

I'm currently developing an online Lean IDE. I tries some existing editor(VSCode, Emacs) and found all of these editor "cannot understand the structure of code"

for example, type following string in VSCode

"
This is a string !"

If I press Ctrl-/ on the second line, VSCode just blindly insert -- at the beginning of line.

I read the Lean code, and I found that Lean use parser combinators. Some tokens are ad-hoc in code (for example, there are many "(" ")" hard-coded)

I also read https://leanprover.github.io/reference/lexical_structure.html, but it's not clear, it doesn't elaborate what the term "Symbol" is, this make me really confusing.

Is there some token specification for Lean4?

[Yury G. Kudryashov]

Lean syntax is extensible on many levels, so the only way to parse lean is to ask the lean server.

[JJ]

that lexical structure reference is for lean 3, also.

[JJ]

depending on what you want to do (how precise do you want to be?), i think your best bet may be to read the source or work off of the vscode-lean syntax highlighter file