Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Defects in color theme and Unicode characters when deleting text #188

Open
GregorPercic opened this issue Aug 3, 2024 · 0 comments
Open

Comments

@GregorPercic
Copy link

GregorPercic commented Aug 3, 2024

When I delete some text in between reloading an .agda file, these two bugs occur:

  1. the color theme becomes inconsistent (and nonsensical),
  2. some Unicode characters (from experience, always those high up in the coding table, such as 𝕍, 𝒫, etc.) turn into gibberish, such as ��.

Reloading fixes both issues. My suspicion is that characters "high up" in the table cause a one-character shift due to having a longer encoding, which the program for the color theme and display of Unicode characters does not take into account.

An example in pictures (normal vs. these two bugs present):

image
image

The source code from the above example is in this repository. I think both bugs can be replicated simply by deleting {_} character by character.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant