Open Melvar opened 9 years ago
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 notifications@github.com 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.
This should work now.
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 likeand uses
\d
, this jumps to the beginning of the line, searches for the:
, then goes back withb
. This places the cursor on the'
offoldl'
, as for purposes of movement the non-blank non-word
char sequence'
counts as aword
. Then, aword
is taken withexpand("<cword>")
. Since the cursor is not on aword
character, this takes the next followingword
, namelyb
, which is then used in the idris client command.The desired behavior is for it to use the identifier
foldl'
instead.