green code after comment

Stream: lean4

[Jovan Gerbscheid]

In VSCode, if I write < followed by a letter in a comment, then the code colouring gets messed up in the rest of the file, turning regular text into green text:

/- <a -/

def foo : Nat := Nat.zero

The last line is completely green. Type-checking and hovering still work fine.

[Marc Huisinga]

This is probably vscode-lean4#369.

[Jovan Gerbscheid]

Indeed, but that mentions it being italic instead of having a different colour.

[Kevin Buzzard]

David's example in the issue is also green for me now (I've mentioned it on the issue).

[Julian Berman]

Dealing with fenced markdown is annoying -- in lean.nvim we disabled it entirely in Lean comments awhile back, hoping to have something more robust later, but I'm not sure things have gotten much better (mainly meaning I think this is still equally hard to do with tree-sitter now).

[Eric Wieser]

I think the highlighter was happy with this in Lean3, though I could be mistaken

[Marc Huisinga]

No, it's broken in vscode-lean as well. We use almost exactly the same grammar for parsing markdown - I just copied it from vscode-lean.

[David Thrane Christiansen]

I think that green vs italic vs other styles is a matter of your theme :)