Interacting within agda code in Atom

[pnlph]

Hi,

i am searching for an Atom package that allows to interact better with language services like go-to-definition.

I found the atom-ide-ui package, but language integrations should be built on top of atom-languageclient.

There is already a list of language packages, and one of them is the ide-haskell-hie.

Is there a way of using this haskell package with agda? Are there other better solutions to approach something like what atom-ide-ui offers?

Thanks!

[banacorn]

Those command language services are a part of what is called the Language Server Protocol.

I've investigated LSP quite a bit and even tried to implement a language server for Agda. However, the protocol is too limited, it only covers a little part of what Agda has to offer.

Of course, if there's a language server for Agda, then the user can use those services like go-to-definition, but he/she would still need agda-mode to cover the rest of the functionalities

[pnlph]

If I understand right, the protocol itself does not provide the basis to build a full implementation of a language server for Agda.

I see that it is possible to create protocol extensions, would be a suitable extension for agda a significant effort?

Once a hypothetical extension is added, would it be easier to implement the language server for agda?

[banacorn]

I'm not sure, even if the extension is added, it'll still be quite an effort.