colour glitch in VS Code

Stream: lean4

[Kevin Buzzard]

On my mac reviewing an FLT PR I ran into the following colour glitch which, for a nice change, I could reproduce:

colours.gif

I restart the file in VS Code and attribute on line 266 goes from blue to yellow (while the orange bars are there) and back to blue (when they disappear). I occasionally see colour glitches but they're usually transient; this one I can reproduce on my mac laptop and ubuntu desktop (it's FLT#773, apologies if this is a known issue, I couldn't find anything like it in the open issues on https://github.com/leanprover/vscode-lean4 which I am assuming is the right place to report this if people want me to)

[Patrick Massot]

Isn’t it simply the usual thing that semantic syntax highlighting is more accurate than the crude approximation you get before the server is ready?

[Julian Berman]

Yeah along perhaps with that I think just because file progress is done for a section (i.e. orange bars go away) that doesn't mean token information has been sent for that section, that's a separate thing sent by Lean to the editor.

[Kevin Buzzard]

Got it, thanks. I hadn't realised that syntax highlighting was that hard (i.e. that it was using the server at all).

[Ruben Van de Velde]

Because of lean's syntax flexibility, the only thing that can really parse lean accurately is lean itself

[Kevin Buzzard]

I see. I'd heard this phrase before but I hadn't realised that it went as far as colours.