Kevin Buzzard (Apr 14 2019 at 14:34):
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 (Apr 14 2019 at 14:38):
Bryan Gin-ge Chen (Apr 14 2019 at 16:29):
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 (Apr 14 2019 at 18:07):
They appear randomly and it's hard to reproduce.
Bryan Gin-ge Chen (Apr 14 2019 at 18:26):
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 (Apr 14 2019 at 18:27):
Good detective work! Thanks!
Patrick Massot (Apr 14 2019 at 19:22):
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
Last updated: May 06 2021 at 22:13 UTC