search

derekelkins / agda-vim

Agda interaction in vim
BSD 2-Clause "Simplified" License
130 stars 47 forks source link

Normalize doesn't seem to do anything (Agda 2.6.0.1) #48

Closed spearman closed 4 years ago

spearman commented 4 years ago

Not sure if this is because the Agda version is too recent. When entering an expression for AgdaNormalize, nothing happens. Typing in gibberish doesn't return an error and entering a valid expression doesn't produce any output either.

derekelkins commented 4 years ago

Assuming you're doing something like :call AgdaNormalize('...') then it will behave the way you describe if you do not provide a valid argument which is one of the strings: "DefaultCompute", "IgnoreAbstract", "UseShowInstance". In other words, if you do, for example, :call AgdaNormalize('') it will prompt you for an expression if the cursor isn't on a hole and then do nothing. Presumably, Agda is returning an error for an invalid option and that error is silently dropped. I probably will not do anything about this.

If :call AgdaNormalize('DefaultCompute'), :call AgdaNormalize('IgnoreAbstract'), or :call AgdaNormalize('UseShowInstance') are behaving as you describe, please reply, but I can't reproduce the issue with those using Agda 2.6.0.1 and vim 8.1.

spearman commented 4 years ago

That was it. The readme shows this by the way:

" C-u C-c C-n -> \n
nnoremap <buffer> <LocalLeader>n :call Normalize("False")<CR>
" C-c C-n -> \N
nnoremap <buffer> <LocalLeader>N :call Normalize("True")<CR>

I was trying to rebind normalize using "False" and "True".

derekelkins commented 4 years ago

Ah, that is an issue. I'll correct the documentation. Agda changed the format for the underlying command some versions back. Thanks.