search

idris-hackers / idris-vim

Idris mode for vim
221 stars 52 forks source link

Fix hole-querying for remaining commands. #73

Closed brianwolfe closed 7 years ago

brianwolfe commented 7 years ago

This lets holes for be recognized appropriately for creation of lemmas. This was broken in https://github.com/idris-hackers/idris-vim/pull/68 and partially fixed in: https://github.com/idris-hackers/idris-vim/pull/71

How was this tested?

I manually tested:

I didn't test the remaining use cases, but it doesn't appear that Idris typically expects the hole name to include the preceding ?

brianwolfe commented 7 years ago

Whoops, there's already a PR open for this. Closing.

stephen-smith commented 7 years ago

So, I didn't apply a change to doc (holes won't have documentation), add missing (can't case analyze a hole), or refine (I've never gotten that to work anyway). But, you seem to have done more testing than me; should I expand my PR to include those commands?

brianwolfe commented 7 years ago

@stephen-smith I think yours is more correct. I just carelessly applied it to each cword attempt. Holes won't have documentation, but ? isn't a beginning of a symbol anyway, so it didn't hurt anything.