Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

In IDE mode, look for a ipkg file before loading #265

Merged
merged 1 commit into from
Jun 10, 2020

Conversation

edwinb
Copy link
Collaborator

@edwinb edwinb commented Jun 9, 2020

This takes the responsibility of finding the ipkg away from IDE mode, which seems sensible given that we can do it ourselves. If there isn't one, it'll load from the local directory as always.

(I won't merge this immediately - please shout if it's likely to break anything. I think it's a better way to go, though, in the end.)

This takes the responsibilty of finding the ipkg away from IDE mode,
which seems sensible given that we can do it ourselves. If there isn't
one, it'll load from the local directory as always.
@jfdm
Copy link
Collaborator

jfdm commented Jun 10, 2020

This is nice.

Just to be clear, and reading the source, the behaviour is not to find the first ipkg file one encounters regardless of name, but try to find the named one.

There is an issue with Idris1 emacs mode in which it gets confused over which ipkg file to use if there are multiple ones present: iirc it finds the first ipkg file regardless of name. Given that we can now explicitly say which one we want to load this should address that issue.

@gallais
Copy link
Member

gallais commented Jun 10, 2020

agda/agda#4526 has taught me that we have to be careful about exploring
the directory tree structure looking for a configuration file.

Hopefully won't be a problem here as people will not be interactively editing
files in a subdirectory of /nix/store/.

@edwinb
Copy link
Collaborator Author

edwinb commented Jun 10, 2020

@jfdm No, it looks for any ipkg in the parent directories. The filename you give findIpkg is the thing you want to load. It returns the path of that file relative to the first .ipkg it finds.

@gallais One problem I have encountered (with --find-ipkg, which vim uses) is finding the wrong .ipkg when working in a subdirectory of the main project. This is why I had to add dummy .ipkg files in the IDE mode tests. A refinement that would probably address this would be to check whether the file you're trying to load is in the appropriate source directory.

@edwinb edwinb merged commit 42676d2 into idris-lang:master Jun 10, 2020
@edwinb edwinb deleted the find-ipkg-ide branch June 10, 2020 12:56
attila-lendvai pushed a commit to attila-lendvai-patches/Idris2 that referenced this pull request Jul 27, 2021
fix typo in docs/tutorial/typesfuns.rst
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants