Open david-christiansen opened 7 months ago
This looks like an oversight in our adjusted Markdown grammar.
In an exciting new development, the y and 99 now seem to be no longer italic, but they're green instead :-) See Zulip thread (note: no doc comment required).
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
and99
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
fromStd
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 ofSyntax.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
Expected behavior:
def y := 99
is highlighted just likedef x := 5
Actual behavior:
def y := 99
is highlighted with extra stylesVersions
[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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.