agda-mode-vscode
agda-mode-vscode copied to clipboard
banacorn
agda-mode on VS Code
A teammate and I used Microsoft Live Share to collaborate on an Agda file. Agda-mode worked well for me, the person who initiated the share, but not my collaborator, who...
I'm imagining having Agda running on a server listening on a port (perhaps using your other project https://github.com/banacorn/agda-language-server) and VSCode running locally with the extension pointed at the server URL...
In emacs loading an Agda file from an already loaded file reached by clicking on link loads the reached file. That is actually quite nice when exploring code. I find...
Agda supports special characters including Unicode characters in names except for reserved ones, and sometimes it's a convention to write names with such characters. Currently autocompletion and case split don't...
I think emacs allows one to use the up and down arrows for the normalisation field, to scroll through the history of previous normalisations. It would be useful to be...
Agda makes it very nice to write condensed mathematical formulae. But it is often very difficult to work out what the precedence of parts of a formulae are if one...
Agda-mode for vscode is a big improvement over emacs by allowing one to see the definitition of any expression by hovering over it with command key pressed. But it would...
I'd be happy to make one, maybe just use the Agda bird icon with correct coloring on both light and dark themes?
The code already supports generating `IOTCM ...` strings with different highlighting levels: https://github.com/banacorn/agda-mode-vscode/blob/c9c24654d2bdbfca7ce9a7bdbf4b8c63f1a9df87/src/Request.res#L91-L98 but they're always called with NonInteractive: https://github.com/banacorn/agda-mode-vscode/blob/c9c24654d2bdbfca7ce9a7bdbf4b8c63f1a9df87/src/Request.res#L105-L109 Could there be a setting to change this?
