Inputting the "agda input prefix" as a literal

[googleson78]

If I set my agda input prefix to e.g. v, how can I input a v? My current prefix is a backtick, and I cannot figure out how to input a backtick into my code 😅

[googleson78]

(backtick is also my localleader, if that's relevant)

[isovector]

I don't think there's any way, today! I'm open to suggestions for what you'd like to happen, though.

[googleson78]

The easiest way to get this, although a bit annoying, is to have a "timeout", i.e. if you press "agda input prefix" and wait for 1s, you just get the prefix input as a literal. This is what maps usually do in vim - if you do

inoremap asdf ...

and then input an a while in insert mode, you'll eventually get the a input as a character after waiting for a bit.

[epeery]

Adding these two lines to the AgdaFiletype function is what I do.

vim.fn['cornelis#bind_input']('<leader>', '<leader>')
vim.fn['cornelis#bind_input'](' ', '<leader>')

This lets me insert the literal form of my leader key by either typing it twice or by pressing space.

I'm using Lua with NeoVim but I would assume that adding the equivalent VimScript would also work:

call cornelis#bind_input("<leader>", "<leader>")
call cornelis#bind_input(" ", "<leader>")

Also note that remapping space causes the leader key to be inserted on timeout. This is what I prefer but some may find the behavior undesirable.

[silky]

Yes, I did exactly what @epeery did. But in the end I got annoyed at typing my localleader twice, so I just changed my agda_input_prefix to tab 😀

I think maybe the secret is to set that value per file-type; I think in Agda I don't type my localleader much, so I don't mind it being that (,, if anyone is curious.)