Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
276 stars 26 forks source link

WIP: `hop.nvim` integration #268

Closed rish987 closed 11 months ago

rish987 commented 2 years ago

Depends on (minor) bug fixes in phaazon/hop.nvim#304. What I've done so far is to map:

All of the above operate from the source code, so you don't have to context-switch to the infoview window and then go back to the original window. There are a number of additional things I want to do (will make a TODO list later) but I wanted to put this PR up now in case there's any early feedback.

asciicast

^ Sorry if that's a bit inscrutable, I'm trying to figure out how to get my terminal to show keystrokes, but essentially what I did was <localleader>jj to go to some in the infoview and see its type, and then <localleader>jd to go-to-definition of Option.

Side note: If you're wondering why I haven't been super active lately, it's because I've been ramping up at a new job where I get to work on Lean full-time! I've settled pretty well at this point and am now finding a healthy balance between work, contributing to neovim, and learning about the Lean 4 implementation with the goal of eventually contributing to its usability aspects. Thanks for your patience!!!

rish987 commented 2 years ago

Also, obviously this relates to #197, we're lucky that @phaazon has since made an official API for us to use! Again, the fixes in phaazon/hop.nvim#304 should stay minor.

Julian commented 2 years ago

Cool! Screenshare looks nice, no concerns yet from me!

Only minor thing is perhaps just put binding those keys behind an if which only runs when hop.nvim is installed, so we don't quash a keybind someone may be using for something else entirely without hop.

rish987 commented 2 years ago

TODO:

Obviously some of these will be more involved than others and so are not all for this PR, just wanted to make a list somewhere that I can keep track of.