search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
169 stars 39 forks source link

Loading can fail silently #106

Open joliss opened 2 years ago

joliss commented 2 years ago

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:

  1. In VS Code, open an Agda project with an Agda file.
  2. Load the file with C-c C-l. This should work.
  3. Go to settings and changeagdaMode.connection.agdaPath to /does/not/exist.
  4. Quit VS Code without closing the current window by pressing Cmd+Q on Mac.
  5. Re-open VS Code. It restores the project window.
  6. Press C-c C-l. This fails without an error message.

Here's a screenshot showing what my window looks like after step 7:

generic-syntax 2022-05-22 17-22-18

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.

banacorn commented 2 years ago

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.