lean.nvim
lean.nvim copied to clipboard
WIP: `hop.nvim` integration
Depends on (minor) bug fixes in phaazon/hop.nvim#304. What I've done so far is to map:
-
<localleader>jj
to hop to interactive elements of the infoview -
<localleader>jd
to use the hop interface to select an element of the infoview that supports go-to-definition (restricting the hints to such elements), and go to that definition. -
<localleader>jh
to use the hop interface to select an interactive element to click (though this is broken at the moment in that the windows don't show up, it's a UI bug I believe)
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.
^ 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!!!
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.
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.
TODO:
- [ ] fix
:LeanHopInfoviewHover
- [ ] allow for the user to provide lean-specific hop configuration options in the
lean.nvim
configuration table that override the options they have globally set forhop.nvim
- [ ] figure out how to deal with overlapping hints that result from notation, e.g. go-to-definition for
Nat × Nat
has a hint for eachNat
, however the· × ·
hint is lost entirely as its hint range starts at the same column as the firstNat
- [ ] properly check that
hop.nvim
is installed before setting up any related functionality (keymaps, commands, etc.) - [ ] make the hop commands work in the infoview itself with similar keymaps
- [ ] on the
hop.nvim
side, add an option to support restricted dimming to only windows where hints are present (right now themulti_windows
option causes all windows to be dimmed) - [ ] parallelize
getGoToLocation
hack (perhaps using a condition variable?)
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.