idris-hackers
vim does not recognize identifiers with '
idris-vim makes use of vim’s concept of a word when determining identifiers to send to idris. This does not by default include ', so, for example, when one has something like
foldl' : (b -> a -> b) -> b -> List' a -> b
and uses \d, this jumps to the beginning of the line, searches for the :, then goes back with b. This places the cursor on the ' of foldl', as for purposes of movement the non-blank non-wordchar sequence ' counts as a word. Then, a word is taken with expand("<cword>"). Since the cursor is not on a word character, this takes the next following word, namely b, which is then used in the idris client command.
The desired behavior is for it to use the identifier foldl' instead.
Any ideas how to persuade vim to do this? Is vimscript expressive enough? As you can probably tell from the interactive bits of vim mode, my knowledge of vimscript is very limited.
On 29 Dec 2014, at 15:50, Melvar Chen [email protected] wrote:
idris-vim makes use of vim’s concept of a word when determining identifiers to send to idris. This does not by default include ', so, for example, when one has something like
foldl' : (b -> a -> b) -> b -> List' a -> b
and uses \d, this jumps to the beginning of the line, searches for the :, then goes back with b. This places the cursor on the ' of foldl', as for purposes of movement the non-blank non-wordchar sequence ' counts as a word. Then, a word is taken with expand("
"). Since the cursor is not on a word character, this takes the next following word, namely b, which is then used in the idris client command. The desired behavior is for it to use the identifier foldl' instead.
— Reply to this email directly or view it on GitHub.
I noticed this breaking on foo' : Nat, where \d added Nat = ?Nat_rhs with the Nat indented to align with the Nat in the line above.
v:beval_text reports the word as foo when I point at it with my mouse in gvim.
