isovector
Inputting the "agda input prefix" as a literal
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 :sweat_smile:
I don't think there's any way, today! I'm open to suggestions for what you'd like to happen, though.
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.
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.
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.)
