Infoview window position after closing a lean buffer

[blindFS]

Here's my workflow:

1. open a lean file with some imports from mathlib
2. press C-] to jump to the dentitions of some type/class/..., which opens another lean file

• so far, the infoview keeps its original position, which is nice

4. :bd to close the file of definition

• I would expect it to jump back to the original lean file with its infoview at the same position
• but it remains with only the infoview window, and I have to manually switch buffer, then resize the window, which is quite laborious

I wonder if there's some smart autocmd infoview window management that I can paste in my config to ease that?

[Julian]

(I assume your C-] is just the default mapping)

bd will delete a buffer, and with it the window it's sitting in. It's never really a useful operation in (neo)vim. If you want to close a window you'd generally use :q, but I'm not sure I understand why the expectation is to go back to your original file regardless of whether you use :bd or :q, in vim when you close a window it just closes, it doesn't bring you back anywhere. Maybe I'm not understanding what you're describing.

But it sounds like you want to use C-o to jump backwards to where you were (see :h jumplist), or to open your definition in a new window (see e.g. :h ^W^]) so that when you close that new window you go back to the first one.

Let me know if I'm misunderstanding what scenario you're describing, or feel free to record your screen and share that if so as well.

[blindFS]

C-O will not close the new buffer, right?

I mean C-] jumps from file A to file B, after reading file B, how can I close file B and jump back to A? :bd is my usual way for that matter when working with other languages.

[blindFS]

TIL lazyvim has a <leader>bd binding which is exactly what I needed, thanks for your help anyway!

[Julian]

Sorry I'm still not 100% sure I follow what you mean by closing a buffer -- there's hiding it (which is what happens when you browse to a different buffer, or when you close a window), there's deleting it (which is :bd which my opinion is is useless but some people use) (and then there's :bw which is even stronger deleting).

There shouldn't be anything different about windows and buffers for Lean / via lean.nvim but again apologies if I'm misunderstanding which scenario you're referring to.

Sounds like you have found a solution which works for you though which I'm glad to hear!

[blindFS]

There shouldn't be anything different about windows and buffers for Lean / via lean.nvim but again apologies if I'm misunderstanding which scenario you're referring to.

It might have something to do with the window management of Lazyvim which I'm not familiar with.

Sounds like you have found a solution which works for you though which I'm glad to hear!

Thanks!