Spin out the `agda-input` part into it's own plugin?

[silky]

Personally, I think it might be useful to have the agda-input.vim functionality as it's own plugin, so it can be enabled in other settings, not necessarily agda.

For example, I may want to:

• Just have fun typing unicode symbols with ease in various documents,
• Annoy my collaborators by using unicode Haskell syntax,
• ???

In any case, I think I'd use it.

If there's interest, I'd be happy to try and lift it out myself, but I can't promise any particular deadline :)

[isovector]

I'm open to this! I often setf agda just to bring those bindings into scope :) I likely won't do any work here, but I'd be happy for a PR.

[googleson78]

https://github.com/chrisbra/unicode.vim might also just have/be a superset of this functionality, but I haven't tried it personally

[silky]

https://github.com/chrisbra/unicode.vim might also just have/be a superset of this functionality, but I haven't tried it personally

It's not quite, because for example with the present setup here you can define multi-character replacements; for example I made one like so:

call cornelis#bind_input("st", "≡⟨⟩")

I suppose another difference is that here there are many ways of typing the same character, which is kind of handy.

[phijor]

I suppose another difference is that here there are many ways of typing the same character, which is kind of handy.

:+1: from me!

Some other advantages I see:

1. We could have a machine-readable source of truth for all substitutions, i.e. generate agda-input.vim from some other file, say a JSON file. This could allow other tools to use the same mappings. Currently, every Agda integration invents its own input mappings.^{(And I recently found myself in a situation where I really needed agda-input in a web project)}
2. We could split substitutions by category, and let the user decide which subset to use. I tend to mistype some abbreviations, and end up with unwanted substitutions. I'd like to disable some of the presets that I know I won't use.

If 1. sounds useful, one could perhaps ask upstream if they are interested in keeping the emacs input in sync from a shared source.

[silky]

Here we go - https://github.com/silky/vim-agda-input

It's just enough to be useful for me. I'm not sure if it's better to delete the code here in this plugin and then force people to install that one (that seems like a worse UX for people coming here for Agda joy), but 🤷🏻 , I'm open-minded.

Thanks @isovector for letting me steal that code! Let me know if you want me to add anything to the readme/etc.