You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I remember agda-vscode maintains an edit-list to correct highlight positions when the user edits the file. But VSCode seems not to fire certain events as user types (instead, it fires a file change event on save).
On save, the server sends the highlight result from SyntaxHighlight to client. The old approach (sending highlight result after C-l C-l) is deprecated.
For every time user edit a file, the LSP unload it. We can do better:
Ctrl+L Ctrl+L
(already done).This is inspired from @agda.
@imkiva wdty
The text was updated successfully, but these errors were encountered: