lean.nvim icon indicating copy to clipboard operation
lean.nvim copied to clipboard

WIP: `hop.nvim` integration

Open rish987 opened this issue 1 year ago • 3 comments

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.

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 avatar Aug 09 '22 22:08 rish987

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.

rish987 avatar Aug 09 '22 22:08 rish987

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.

Julian avatar Aug 10 '22 11:08 Julian

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 for hop.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 each Nat, however the · × · hint is lost entirely as its hint range starts at the same column as the first Nat
  • [ ] 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 the multi_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.

rish987 avatar Aug 11 '22 01:08 rish987