Skip to content

Toward Idris2 support on Vim, could use advice and help #92

@cheery

Description

@cheery

Hi. I started working on Vim8/Idris2 modification that interacts through --ide-mode. I've gotten things working badly, but there are few odd things about the function of the IDE mode that I don't figure out.

https://github.com/cheery/idris-vim
https://github.com/cheery/idris-vim/blob/master/ftplugin/idris.vim

What am I supposed to do when I reload a file through idris-mode? Sometimes it's giving me 'return' response and other times it's not doing that. The IDE protocol documentation doesn't tell me what kind of choreography should the editor carry out.

The another question is with the "make-case". It's giving me a nice "fill-this-in" structure. How do I properly do the replacement though?

Also interested what do you think of the code. It's asyncronously running and I tie it up together with guard functions that retry on a task when progress is made.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions