search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

Set the cursor to the goal when updating infoview windows. #279

Closed Julian closed 1 year ago

Julian commented 1 year ago

The main motivation for this is that it makes the goal visible when the infoview is full of many lines (e.g. there are many hypotheses). In particular this happens a lot on vertical displays with horizontal infoviews (that don't offer many lines).

Closes: #240

Julian commented 1 year ago

Thanks! I have to check the aligning-while-interacting behavior still I was planning on doing so before either pinging or merging, will do it in a bit (for now been using this for a day or two of light leaning and haven't seen any other issues yet).

I agree the alignment should happen at a higher level, but I'm still somewhat unhappy with the whole path to rendering -- it seems to happen "bottom up" with Pins being responsible for rendering, when I think it should live up in infoviews, and Pins be somewhat behaviorless. But still needs more thought... (Infoview:render doesn't exist at the minute, maybe it did previously, but yeah it's something I was thinking about as well when looking at this)