search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

Interacting within agda code in Atom #121

Open pnlph opened 4 years ago

pnlph commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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