VSCode extension: alpha in a box

Stream: general

[Kevin Buzzard]

I'm giving a talk to some computer scientists in 3 hours and I thought I'd show them how good I was at lists. But all my alphas are in boxes in VS Code so right now I've reverted to betas. What have I done wrong?

Screenshot from 2025-02-18 09-47-45.png

[Marc Huisinga]

Close the tab and re-open it

[Marc Huisinga]

This is probably vscode#234617 / vscode#231224 / vscode#240567

[Marc Huisinga]

The box issue should be fixed in the next VS Code release, the issue with VS Code inputting the incorrect amount of spaces in the same situation still needs to be fixed by VS Code

[Kevin Buzzard]

Thanks! I knew there was a hack but I couldn't remember the details, I tried restarting the file, restarting the server and restarting VSCode and none of them worked, so I concluded that I'd forgotten the hack and asked here :-)

[Rémy Degenne]

If you have several files open, just clicking another tab and then coming back solves the issue (at least it does for me).

[Marc Huisinga]

This solves the box issue, but it won't solve the issue of VS Code inputting the incorrect amount of spaces when you hit Tab

[Rémy Degenne]

Oh ok, thanks for the clarification. I did not know there was also an issue with spaces.

[Marc Huisinga]

When you start VS Code and there's a file open, it will basically ignore all the configuration defaults that we set for the Lean language. We set a couple of these, and both the box issue and the space issue are caused by VS Code ignoring us overriding its default behavior.

[Marc Huisinga]

(The box setting isn't even listed in the manual, it's 'Editor > Unicode Highlight: Ambigious Characters' that VS Code ignores here)