agda-mode-vscode
agda-mode-vscode copied to clipboard
Syntax highlighting doesn't update correctly when filling a hole until the file is reloaded with C-c C-l
After filling a hole with something, and hitting C-c C-SPC
(give) or C-c C-r
(refine) the syntax highlighting is extremely wrong, with individual characters or groups of characters being highlit willy-nilly:
and is only correct after loading again with
C-c C-l
I see this not only on holes but with many cases. Are there any ideas why this happening and how could be solved?