Closing the infoview buffer causes errors

[gebner]

When I (accidentally) close the infoview buffer, the following error repeats very quickly:

Error executing vim.schedule lua callback: /home/gebner/lean.nvim/lua/lean/infoview.lua:61: Invalid buffer id: 3

It would also be nice to have commands to reopen or toggle the infoview.

[Julian]

Toggling is present already -- it's mapped to <localleader>i if you have mappings = true in the config (or if you called .use_suggested_mappings()). Or you can map lua require'lean.infoview'.toggle() to whatever you'd like obviously.

The first one is a known issue though yeah -- I put it in a subcomment of #17 ("automatically disable the infoview when it is :q'ed") but probably better to leave this open and have it be its own issue.

Shouldn't be hard to fix.

[gebner]

Then I misread the subcomment! I thought you meant calling :q on the lean buffer would automatically close the infoview, which would also be useful.

[Julian]

Ah! Yes agree on that one too -- I think that one we should make be configurable, I go back and forth on whether I want vim to autoquit if the infoview is the last buffer open -- sometimes I mean to continue opening some lean file and sometimes I'm done, but if we make it configurable I think that one's also a good idea!