agda-mode-vscode icon indicating copy to clipboard operation
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

Open natronium opened this issue 2 years ago • 1 comments

syntax

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: 04-after-Cc-CSPC and is only correct after loading again with C-c C-l

natronium avatar Nov 18 '21 19:11 natronium

I see this not only on holes but with many cases. Are there any ideas why this happening and how could be solved?

uhbif19 avatar Jun 26 '23 12:06 uhbif19