search

derekelkins / agda-vim

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

Add support for Cmd_helper_function #32

Closed andrejtokarcik closed 6 years ago

andrejtokarcik commented 6 years ago

Displays the type signature of helper function. The feature is mapped to <LocalLeader>h.

There is a related commit in my repo that automatically yanks the signature into a specific register and allows the user to paste it immediately using <LocalLeader>p. I may add it to this pull request if you'd like.

FWIW, the feature (as present in Emacs mode) can be seen in action in this lecture.

derekelkins commented 6 years ago

Thanks. I'll have to look at some stuff for the copy/paste. It definitely doesn't make sense to make the user have to copy the text from a window, but I don't want random commands smashing registers so I'll have to see what else does info-action-and-copy. I may make it a little more flexible (i.e. being able to specify which register to use) and/or a little more noisy (I think an echo will be noisy enough without being annoying if it does what I think). The <LocalLeader>p mapping might be a bit more opinionated than I'd like, but I'd have to play with it and see.

andrejtokarcik commented 6 years ago

Yeah, I thought exactly the same (about overwriting registers) and that's why I didn't include the other commit right away.

As far as I can tell, info-action-and-copy indicates that the client (editor) should not only print the text but also add it to the clipboard.

Thanks for your quick response!