VS Code ignores "editor.unicodeHighlight.ambiguousCharacters": false extension language setting after startup

[mhuisi]

Does this issue occur when all extensions are disabled?: No

• VS Code Version: 1.95.3
• OS Version: Fedora Linux 40, 6.10.12-200.fc40.x86_64

In the VS Code extension for the Lean 4 theorem prover, we set editor.unicodeHighlight.ambiguousCharacter to false for Lean documents since Lean code tends to contain lots of Unicode characters and these boxes make Unicode-heavy code very difficult to read.

Since somewhat recently, users have been reporting that despite us disabling this setting, they see boxes around Unicode symbols right after launching VS Code, i.e. in the last active editor when closing VS Code previously. These boxes disappear as soon as the full text editor state is changed (e.g. by switching the visible tab and back, or by toggling the "Render Control Characters" setting), and the issue can be worked around by also disabling this setting in the user settings.

Steps to Reproduce:

1. Install the Lean 4 extension (I suspect a minimal extension that contributes a language and "editor.unicodeHighlight.ambiguousCharacters": false for it will do, but I haven't tried) on blank user settings.
2. Open an untitled document, set the language ID to lean4 and enter the character ℝ.
3. Close VS Code.
4. Re-open VS Code.
5. Observe that the ℝ is now surrounded by a box.

[RedCMD]

dup #231224