search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Syntax highlighting adds an odd box around lower-case unicode letters #905

Open RalfJung opened 3 weeks ago

RalfJung commented 3 weeks ago

I often use unicode letters in my Coq identifers, to better match what we do on paper. This works fine in Coq, but the syntax highlighting of this extension draws a box around some these characters:

image

This makes them look like some sort of error, and also makes them hard to read.

In a plain text file these letters look just right, so it seems to be something specific to what VsCoq does in .v files. This seems to be font-independent; I tried two different monospace fonts and they both show this effect.

4ever2 commented 3 weeks ago

I don't think this is anything specific to VsCoq, it seems to be because of the editor.unicodeHighlight.ambiguousCharacters setting. When enabled it will highlight any ambiguous unicode characters in all non plaintext/markdown files.

RalfJung commented 3 weeks ago

Thanks for pointing that out! That helps indeed. :) I have no clue why vscode thinks σ could be confused with another charcacter (but, say, Λ could not)... but now I can at least disabled this behavior.