Skip to content

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

Description

@RalfJung

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions