Broken semantic highlighting

Stream: lean4

[Patrick Massot]

Is it only me or is semantic highlighting broken in the latest version of the VSCode extension? @Marc Huisinga

[Patrick Massot]

I had to reload the VSCode window to bring it back.

[Marc Huisinga]

I certainly didn't touch anything related to semantic highlighting in quite a while. What's your VS Code version? I'm wondering if VS Code may have changed something about their implementation.

[Patrick Massot]

1.91.1

[Marc Huisinga]

I wonder if it's this: https://github.com/microsoft/vscode/issues/221423

[Marc Huisinga]

... or this: https://github.com/microsoft/vscode/issues/211369

[Marc Huisinga]

If you encounter this issue a lot, could you downgrade your VS Code version to 1.90.x and see if the issue still appears there?

[Patrick Massot]

Thanks I will investigate.

[Marc Huisinga]

@Patrick Massot Did you manage to find out more about this?

[Patrick Massot]

I’m no longer using VSCode on a daily basis, I switched to vim. I’ll be able to tell you more when I resume my work on my teaching material. But probably that won’t be very soon, I’m currently overwhelmed by the start of academic year.