Agda Support - Githubissues

helix-editor / helix

A post-modern modal text editor.

https://helix-editor.com

Mozilla Public License 2.0

34k stars 2.51k forks source link

Agda Support #4465

Open oati opened 2 years ago

oati commented 2 years ago

I don't exactly know what editor features helix would need for a complete agda experience. I'm hoping someone more experienced with agda could help with this.

Agda has an issue for LSP support: https://github.com/agda/agda/issues/3758 There is an implementation: https://github.com/banacorn/agda-language-server

It seems like helix would need

unicode input (although you could just use a compose key)
support for holes
special commands and messages (this would probably be more appropriate as a plugin, unless LSP supports language-specific custom commands)

I also don't know how much should be handled by the LSP server and not helix.

Possibly relevant: https://github.com/microsoft/language-server-protocol/issues/1414

pretentious7 commented 2 years ago

I'd started on this in a branch (only stubs im afraid) https://github.com/helix-editor/helix/pull/3092

I'd be happy to collaborate, but I'm also an agda novice.

blitzerr commented 1 year ago

@pretentious7 thank you for doing this. Any further progress on this one ? I am unsure about how actively ASL is being developed. Is there any chance we can incorporate the Agda-mode like they have for emacs ?

pretentious7 commented 1 year ago

I got a bit bamboozled by the als source (and agda in general...), I'll make another go of it in a couple months.

I'd like agda-mode type hole completion and stuff would be cool.

omentic commented 1 year ago

@pretentious7 Were you ever able to get als working?

I have pretty-good syntax highlighting working in #8285. I've been trying to get it to highlight function implementations to unfortunately no avail yet. The LSP has absolutely been mind-boggling though - I can't figure out what it's doing, let alone why it doesn't work - it seems to be failing to handle even basic file-was-saved events?

pretentious7 commented 1 year ago

@pretentious7 Were you ever able to get als working?

I have pretty-good syntax highlighting working in #8285. I've been trying to get it to highlight function implementations to unfortunately no avail yet. The LSP has absolutely been mind-boggling though - I can't figure out what it's doing, let alone why it doesn't work - it seems to be failing to handle even basic file-was-saved events?

Same here... I switched to emacs about a year back, though, and agda-mode is fine for me.

omentic commented 1 year ago

Good to know :slightly_frowning_face: I have a sneaking suspicion that it relies on some emacs-specific implementation...

omentic commented 1 year ago

(the function highlighting issue turned out to be a bug in tree-sitter core. still have yet to figure out als)