Feature request: Jump to definition, Ctrl-Click. about idris-vscode HOT 4 OPEN

Go to definition is supported by idris2-lsp-vscode. However, installing the LSP can be a bit tricky.

from idris-vscode.

Hi, thanks for making an issue.

I'm not aware of any simple way to implement this. This extension is mostly a wrapper around Idris’s IDE protocol, and I don't think it exposes the information I would need. I'll have a think though.

In the meantime, you could try the lsp extension michaelmesser recommended. The language server has some functionality that the IDE protocol doesn't, although the last time I looked it still had some missing features. I'm not sure how easy it is to run the two extensions side-by-side — I need to investigate that and update the readme.

from idris-vscode.

I don't think it would be a good idea to run the extensions side by side. I will have some time over the next month to work on improving the LSP so let me know what is missing.

from idris-vscode.

@meraymond2 Would it be a good idea to implement this in idris2 compiler and add a new command in language protocols? 

from idris-vscode.