dreaded red blocks of death are back

Stream: general

[Kevin Buzzard]

In VS Code I sometimes get a red rectangle, typically after I've written something with a syntax error. This is not the same as a red underline -- it's a full red background on one or more characters. The only way I can get rid of it is to mash the keyboard creating an error on the pane on the Lean messages pane on the right, and then to hover over the red writing in that pane explaining the error message. I've been doing this for a month or so; VS Code used to do this back in 2017 but I've not seen the behaviour for ages until recently.

[Kevin Buzzard]

red_rectangle.png

[Bryan Gin-ge Chen]

A few months back I fixed the old code in the extension that shows these red rectangles. They're only supposed to appear when you're hovering over a message (error, warning, or info) in the info view panel though, so something is clearly broken. Do you know what else might be triggering them?

[Kevin Buzzard]

They appear randomly and it's hard to reproduce.

[Bryan Gin-ge Chen]

OK, I think I've found the bug. To reproduce, you have to type something which creates an error message in the info view exactly underneath your mouse cursor, and then edit the code so that the message goes away before you move your mouse away from that spot. The extension doesn't properly clean up the hover decoration and so it gets stuck. Thanks for reporting this! I'll try to PR a fix soon.

edit: Here it is

[Kevin Buzzard]

Good detective work! Thanks!

[Patrick Massot]

Oh, fixing this would be great! My students see it all the time. I usually switch to another file and switch back. I never suspected this was a vscode-lean bug, I thought this was VScode alone