Description

When a docstring contains something that could be HTML but isn't, the rest of the file is highlighted as if it were part of the docstring. This leads to incorrect fonts.

Here's a screenshot:

Note that y and 99 are italic.

Using the "inspect scopes" feature, it seems that the doc comment is taken to extend past its bounds:

Context

When working with #guard_msgs from Std to test a parser, it's common to have <missing> occur in doc comments, because that's the output of a failing parser (the standard pretty-printing of Syntax.missing). After the first occurrence of it, the rest of the file is incorrectly highlighted.

I think this is because it's trying to parse the contents as Markdown, which allows arbitrary HTML to be embedded, and then that parsing extends beyond the closing -/.

This issue doesn't happen in other editors, so I'm pretty sure it's the VS Code plugin, rather than the language server sending bogus semantic tokens.

Steps to Reproduce

1. Create a new file
2. Insert the below text
3. Observe the coloring

def x := 5
/--
Doc comment that mentions `missing`:
  <missing>
-/
def y := 99

Expected behavior:

def y := 99 is highlighted just like def x := 5

Actual behavior:

def y := 99 is highlighted with extra styles

Versions

[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)]
0.0.121

[Output of lean --version in the folder that the issue occured in]

Lean (version 4.4.0-nightly-2023-11-16, commit b770060b9e1a, Release)

[OS version]

Mac OS 13.6.2

Additional Information

None

Impact

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