agda-mode-vscode
agda-mode-vscode copied to clipboard
banacorn
agda-mode on VS Code
Additionally, lines that contained trailing whitespace were trimmed.
I'm running on Windows 10 - after having downloaded and installed the agda-language-server and typed C-c C-l on my .agda file, I get the following message Connection Error: Client Internal...
Just a quick heads-up to let you know that in the Visual Studio Marketplace description, I noticed "Shortcut" was typoed as "Shortcurs". I see the same typo here in the...
When the agda-mode extension is enabled, syntax highlighting and the "Open Preview" option (Ctrl+Shift+V) stop working for `.lagda.md` files.
When switching between projects that use different versions of Agda, I have to clear the agda path and restart vscode every time, which is annoying. If there is a use...
Error: ``` No backend called 'GHC' (installed backends: GHCNoMain, QuickLaTeX) ``` but I see that's the default in my setting:  crossposted: https://stackoverflow.com/questions/71876445/how-does-one-use-ghc-in-agda-with-vscode
 Please save me, I love cut and paste!
VSCode is not working reliably with adga-mode. I have an up-to-date copy and am using Agda version 2.6.1.1-fce01db. My experience of today: VSCode worked normally for a few hours, then...
There are cases where loading an Agda file with C-c C-l can fail silently, without any error message or indication that something went wrong. I managed to reproduce it in...
Hi, I will attach a screenshot to show you the issue: The theme is called "Light+"
