Configurably autoclose the infoview if it has no Lean buffers updating it

[Julian]

Add a configuration option infoview.autoclose = true (default) which indicates the infoview should be closed if no Lean buffers are updating it anymore (e.g. particularly if it is the last remaining window).

[frangio]

I've set this up in my config with:

local infoview = require('lean.infoview').get_current_infoview()
if infoview then
  local tab_wins = vim.api.nvim_tabpage_list_wins(0)
  local non_info_wins = vim.tbl_filter(function (w) return w ~= infoview.window end, tab_wins)
  if #non_info_wins <= 1 then
    infoview:close()
  end
end

Not sure if this is all that's required. I can submit a PR but I'm not sure how to test this.

[Julian]

I am behind on lots of stuff so I haven't yet thought about this again -- I think what you have looks good for sticking in your own config but probably would want to be thought out very slightly more for actually merging.

Specifically -- I think it's worth at least (re)considering whether to autoclose if it's the last window or whether, as the title here suggests, there's no other lean windows open. E.g. if I have foo.lean, an infoview, and bar.md open, I suspect that still might want to autoclose the infoview if I close foo.lean -- or better, given that I could see a user wanting both, probably we want to think about how or if we could help support a hook that lets the user decide.

I'm sure the "full implementation" is not far away from what you shared, but just want to set aside a tiny bit of time (or welcome more thoughts from you our anyone). Please feel free to ping if I don't follow up soon and you're keen, as if it stays open for much longer I'm inclined to nevertheless welcome what you have!

[frangio]

if I have foo.lean, an infoview, and bar.md open, I suspect that still might want to autoclose the infoview if I close foo.lean

I totally see what you mean now after working with this setup for a bit. I think that is the behavior I would want.

I can see this as having three options for infoview.autoclose like false, 'eager', 'last-only' or something.

[frangio]

I've changed my setup to the following, though this only implements the more eager version of autoclose. I also disabled the default autoopen behavior because for this setup it needs to be triggered in BufWinEnter rather than BufEnter.

local group = vim.api.nvim_create_augroup('LeanAutoOpenClose', {})

vim.api.nvim_create_autocmd('BufWinEnter', {
  group = group,
  pattern = {'*.lean'},
  callback = function ()
    require('lean.infoview').open()
  end
})

vim.api.nvim_create_autocmd({'BufWinLeave', 'QuitPre'}, {
  group = group,
  pattern = {'*.lean'},
  callback = function ()
    local infoview = require('lean.infoview').get_current_infoview()
    if infoview then
      local tab_wins = vim.api.nvim_tabpage_list_wins(0)
      local lean_wins = vim.tbl_filter(function (w)
        local buf = vim.api.nvim_win_get_buf(w)
        local buf_ft = vim.api.nvim_buf_get_option(buf, 'filetype')
        return buf_ft == 'lean'
      end, tab_wins)
      if #lean_wins <= 1 then
        infoview:close()
      end
    end
  end
})

I suppose one additional complexity not handled here is that if the user explicitly closes the infoview it should not be reopened automatically.

[frangio]

Another question is what should happen with lean://stderr windows.

[stephen-huan]

I've been using #43 (comment), and it works great with a few modifications: (1) using

vim.api.nvim_create_autocmd('BufWinEnter', {
  group = group,
  pattern = {'*.lean'},
  callback = function ()
    require('lean.infoview').open()
  end
})

with infoview = { autoopen = false } causes infoviews to "hang" whenever a new lean file is opened, e.g.

• open a lean file
• make a new tab and open another lean file
• go back to the first file
• infoview no longer updates

or

• open a lean file
• :split another.lean
• first buffer's infoview no longer updates

Simply removing this and using infoview = { autoopen = true } again fixes this.

Having both '{'BufWinLeave', 'QuitPre'} means it sometimes activates twice on the same close (see #346).

• open a lean file
• make a new tab and open another lean file
• close the file with :q
• back at the first file, infoview closed as well

If just BufWinLeave is set, there's another problem.

• open a lean file
• make a new tab and open the same lean file
• close the file with :q
• left with just infoview window in the tab

since BufWinLeave only runs if the buffer is no longer visible in any window (:help BufWinLeave)

BufWinLeave			Before a buffer is removed from a window.
				Not when it's still visible in another window.

The solution is to just activate on QuitPre; I could be missing some edge cases.

With the aforementioned modifications the snippet looks like

local group = vim.api.nvim_create_augroup('LeanAutoOpenClose', {})

vim.api.nvim_create_autocmd('QuitPre', {
  group = group,
  pattern = {'*.lean'},
  callback = function ()
    local infoview = require('lean.infoview').get_current_infoview()
    if infoview then
      local tab_wins = vim.api.nvim_tabpage_list_wins(0)
      local lean_wins = vim.tbl_filter(function (w)
        local buf = vim.api.nvim_win_get_buf(w)
        local buf_ft = vim.api.nvim_buf_get_option(buf, 'filetype')
        return buf_ft == 'lean'
      end, tab_wins)
      if #lean_wins <= 1 then
        infoview:close()
      end
    end
  end
})

with infoview = { autoopen = true }.