search

aya-prover / aya-vscode

~ VSCode extension for Aya Prover
GNU General Public License v3.0
7 stars 2 forks source link

Random rainbow highlights when editing after first-time load #15

Open imkiva opened 2 years ago

imkiva commented 2 years ago

Related code: https://github.com/banacorn/agda-mode-vscode/blob/master/src/Highlighting.res#L87

It's very annoying to keep semantic tokens in sync with user edits manually. I decide to simply remove highlights when editing until we have a better way to update highlights as user types, or we just compromised.

imkiva commented 2 years ago

Reopen since it is not really fixed.

ice1000 commented 2 years ago

I am happy with this solution! It seems okay