agda-mode-vscode
agda-mode-vscode copied to clipboard
Loading can fail silently
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 the following way:
- In VS Code, open an Agda project with an Agda file.
- Load the file with C-c C-l. This should work.
- Go to settings and change
agdaMode.connection.agdaPath
to/does/not/exist
. - Quit VS Code without closing the current window by pressing Cmd+Q on Mac.
- Re-open VS Code. It restores the project window.
- Press C-c C-l. This fails without an error message.
Here's a screenshot showing what my window looks like after step 7:
This might seem like an obscure corner case, but I think there are more cases where this happens -- this is just one way that I managed to reproduce it. I've had this behavior a bunch while trying to get Agda running for the first time, and it was a source of confusion for me.
Thank you for this detailed step-by-step reproduction!
In step 5, after opening the editor, you should see a black panel like in the screenshot. If you close that blank panel, step 6. should work.
VS Code used to "reuse" that blank panel so everything would appear normal, but now VS Code has changed its behaviour recently, and I'm not sure if it's possible to restore this.