Add support for addClause and other commands on unsaved files

[ruippeixotog]

If I create a new file, set the language to Idris, add the following content:

import Data.Vect

vectZip : Vect n a -> Vect n b -> Vect n (a, b)

And try to run idris.addClause on vectZip, it gets filled with:

import Data.Vect

vectZip : Vect n a -> Vect n b -> Vect n (a, b)
: openFile: does not exist (No such file or directory)

The same thing happens with idris.proofSearch and probably other commands.

[meraymond2]

Hi, thanks for raising an issue 👍

You are correct that it does not handle unsaved files, the Idris IDE process does not read from a buffer, it reads directly from disk, and I just pass it a file name. I thought about this while I was initially writing the plugin but I don't think I found a solution I was happy with. Where I wasn't sure what users' preferred behaviour would be, I opted to be as uninvasive as possible.

I think that today, my preferred solution would be to just auto-save before running any commands that read the buffer, but with a configuration option to select that behaviour from always, prompt and never. How does that sound?

I'm fairly certain #25 is the same issue, but I'll leave it open for now.

Also, the : openFile: does not exist (No such file or directory) is a bug, and I've made a separate issue for myself to fix that.

[ruippeixotog]

Thanks for the detailed answer! It's rather unfortunate that the LSP only works on files from disk, it really hinders the development experience... In some occasions I'd rather test different things without saving the file, and when I am using a completely new one (e.g. as a scratch file to try out stuff) it won't be possible for it to auto-save. Are you aware of any feature request on Idris for this?

In any case, I think that a configuration option would be a good idea 🙂

[meraymond2]

Are you aware of any feature request on Idris for this?

There is some ongoing discussion about improvements to the IDE Mode, which is Idris's equivalent to the LSP. I can raise up the possibility of loading a text buffer — it would definitely be a nice feature to have.

I'm wondering if there's a way to get around it with temporary files, but I expect it would be quite fiddly. I'll keep thinking about it. For now I'll start working on the autosave/prompt feature.

[meraymond2]

The autosave feature is in the latest release.Let me know if you have any problems with it.

[ruippeixotog]

Works like a charm, thanks @meraymond2!