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.

[crumbtoo]

I'm quite interested! I was going to hack something together using unicodeit, but I would much prefer this :3

[phijor]

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

👍 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.