The less-than sign followed by a non-space character causes a comment to render incorrectly

[ShreckYe]

Description

See the code:

/-
<a comment
comment
 -/

example := trivial

Context

no info

Steps to Reproduce

1. copy and paste the code above into a .lean file in a Lean project in VS Code
2. observe that the block comment is not rendered properly all in green
3. change the block comment to a one-line comment and see that the issue persists
4. hover the caret in the code and see that Lean InfoView shows the correct info, so the compiler works correctly here

Expected behavior: the comment should be all in green

Actual behavior: < is in gray, the following character is in blue, the text after is in cyan, and the closing / is in red

Versions

Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu): v0.0.209
Output of lean --version in the folder that the issue occured in: Lean (version 4.22.0, arm64-apple-darwin23.6.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05, Release)
OS version: macOS Sequoia 15.6.1

Additional Information

no info

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[mhuisi]

Related: #369