VSCode unicode characters highlight box

Stream: general

[Niklas Halonen]

Hi,

For anyone else running into this issue where common math symbols are highlighted with an orange box, I have a solution for you: try disabling Editor › Unicode Highlight: Ambiguous Characters.
vscode setting

Here is an example from Mathlib on how it looks on my machine with the setting turned on:
example

[Julian Berman]

My memory vaguely says that @Bhavik Mehta had this issue as well. I'm no VSCode expert -- is this setting turned on or off by default, or did the default change perhaps depending on when you installed VSCode? If it's on, why don't more people complain about seeing these? It seems pretty harmful to Lean use; maybe vscode-lean should warn if it's turned on if so?

[Marc Huisinga]

We disable it for Lean documents (that's the "Modified elsewhere"). I've seen several people have this issue recently - not sure why VS Code suddenly decides to ignore our default settings.

[Bhavik Mehta]

I think I did have this, but it went away at some point; I recall I did the same thing as Niklas to resolve it.

[Marc Huisinga]

Do you have any other extensions installed that might interfere with this setting? What does your settings.json contain? You can open it by navigating to the settings page and then clicking this button:
image.png

[Niklas Halonen]

@Julian Berman: On my home-manager setup it was enabled by default, don't have info on other distributions, but it probably means it uses VSCode's defaults. It's also worth noting that the issue goes away just by switching tabs until reopening VSCode.

[Niklas Halonen]

@Marc Huisinga: I don't think I have, but I'm not interested in troubleshooting this now. Here is my config (under userSettings: https://gitlab.com/niklashh/nix-notes/-/blob/69a5dc6d21de9401747134dbaf0dfee710f81919/modules/users/programs/codium.nix

[Michael Stoll]

I also observe this. It goes away after clikcing on "Render Control Characters" in the "View --> Appearance" menu entry. Strangely, this is independent of the status (check-mark or not) show in the menu (clicking on it flips the status and teh display, but the two seem not to be correlated).

[Marc Huisinga]

Did this issue ever occur to any of you in a file after opening VS Code?
I can reproduce it, but only in the text editor that is visible right after opening VS Code (i.e. the last one I had open before I closed it). As soon as I switch tabs or change any of the editor settings, it goes away.

[Michael Stoll]

I can confirm that it goes away when switching tabs (also when switching to another tab and then back).

[Marc Huisinga]

I've reported this here: https://github.com/microsoft/vscode/issues/234617

Chances are pretty slim that the VS Code team will work on this, but we'll see.