Implement infoview autoclose.

README.rst

@@ -187,6 +187,8 @@ In e.g. your ``init.lua``:
         enable = true,
         -- Automatically open an infoview on entering a Lean buffer?
         autoopen = true,
+        -- Automatically close and infoview when leaving from its last associated Lean file?
+        autoclose = true,
         -- Set the infoview windows' widths
         width = 50,
       },

lua/lean/infoview.lua

@@ -5,7 +5,7 @@ local is_lean_buffer = require('lean').is_lean_buffer
 local set_augroup = require('lean._util').set_augroup
 
 local infoview = { _by_id = {} }
-local options = { _DEFAULTS = { autoopen = true, width = 50 } }
+local options = { _DEFAULTS = { autoopen = true, width = 50, autoclose = true} }
 
 local _DEFAULT_BUF_OPTIONS = {
   bufhidden = 'wipe',
@@ -41,6 +41,16 @@ end
 ---@param open boolean: whether to open the infoview after initializing
 function Infoview:new(id, width, open)
   local new_infoview = {id = id, width = width}
+
+  -- a set with a counter method
+  new_infoview.lean_windows = {}
+  setmetatable(new_infoview.lean_windows, { __index = {
+    get_count = function()
+      local count = 0
+      for _, _ in pairs(new_infoview.lean_windows) do count = count + 1 end
+      return count
+    end}})
+
   self.__index = self
   setmetatable(new_infoview, self)
 
@@ -69,7 +79,7 @@ function Infoview:open()
   end
   -- Make sure we notice even if someone manually :q's the infoview window.
   set_augroup("LeanInfoviewClose", string.format([[
-    autocmd WinClosed <buffer> lua require'lean.infoview'.__was_closed(%d)
+    autocmd WinClosed <buffer> lua require'lean.infoview'._by_id[%d]:close()
   ]], self.id), 0)
 
   vim.api.nvim_set_current_win(window_before_split)
@@ -109,13 +119,20 @@ end
 function Infoview:focus_on_current_buffer()
   if not is_lean_buffer() then return end
   if self.is_open then
-    set_augroup("LeanInfoviewUpdate", [[
-      autocmd CursorHold <buffer> lua require'lean.infoview'.__update()
-      autocmd CursorHoldI <buffer> lua require'lean.infoview'.__update()
-    ]], 0)
+    set_augroup("LeanInfoviewUpdate", string.format([[
+      autocmd CursorHold <buffer> lua require'lean.infoview'.infoview._by_id[%d]:update()
+      autocmd CursorHoldI <buffer> lua require'lean.infoview'.infoview._by_id[%d]:update()
+    ]], self.id, self.id), 0)
   else
     set_augroup("LeanInfoviewUpdate", "", 0)
   end
+  self.lean_windows[vim.api.nvim_get_current_win()] = true
+end
+
+-- Clears the given window, possibly autoclosing this infoview if it was the last remaining one.
+function Infoview:__clear_win(win, do_not_close)
+  self.lean_windows[win] = nil
+  if not do_not_close and options.autoclose and self.lean_windows.get_count() == 0 then self:close() end
 end
 
 --- Update this infoview's contents given the current position.
@@ -154,12 +171,6 @@ function Infoview:render()
   vim.api.nvim_buf_set_option(self.bufnr, 'modifiable', false)
 end
 
---- Update the infoview contents appropriately for Lean 4 or 3.
---- Normally will be called on each CursorHold for a buffer containing Lean.
-function infoview.__update()
-  infoview._by_id[get_id()]:update()
-end
-
 --- Retrieve the contents of the infoview as a table.
 function Infoview:get_lines(start_line, end_line)
   if not self.is_open then return end
@@ -190,40 +201,65 @@ function infoview.close_all()
   end
 end
 
---- An infoview was closed, either directly via `Infoview.close` or manually.
---- Will be triggered via a `WinClosed` autocmd.
-function infoview.__was_closed(id)
-  infoview._by_id[id]:close()
-end
-
 --- Enable and open the infoview across all Lean buffers.
 function infoview.enable(opts)
-  options = vim.tbl_extend("force", options._DEFAULTS, opts)
+  options = vim.tbl_extend("keep", opts, options._DEFAULTS)
   set_augroup("LeanInfoviewInit", [[
-    autocmd FileType lean3 lua require'lean.infoview'.make_buffer_focusable()
-    autocmd FileType lean lua require'lean.infoview'.make_buffer_focusable()
+    autocmd FileType lean3 lua require'lean.infoview'.__make_buffer_focusable()
+    autocmd FileType lean lua require'lean.infoview'.__make_buffer_focusable()
   ]])
 end
 
+local __last_win
+
+-- When a lean buffer associated with this infoview BufLeave's, we may want to update lean_windows.
+function infoview.__lean_buffer_left()
+  __last_win = vim.api.nvim_get_current_win()
+  -- BufEnter is always triggered after BufLeave
+  vim.cmd(string.format([[ autocmd BufEnter * ++once lua require'lean.infoview'.__lean_buffer_left_post(%d) ]],
+    get_id()))
+end
+
+-- Actually determines whether to update lean_windows after the inevitable BufEnter following __lean_buffer_left.
+-- TODO: Ideally this would be a local function to __lean_buffer_left but sadly neovim doesn't
+-- have very good Lua autocmd integration yet :(
+function infoview.__lean_buffer_left_post(id)
+  -- if the original window no longer shows a lean buffer, remove it from the list
+  if not (vim.api.nvim_win_is_valid(__last_win) and is_lean_buffer(vim.api.nvim_win_get_buf(__last_win)))
+  then
+    if infoview._by_id[id] then infoview._by_id[id]:__clear_win(__last_win) end
+  end
+  __last_win = nil
+end
+
 --- Configure the infoview to update when this buffer is active.
-function infoview.make_buffer_focusable()
+function infoview.__make_buffer_focusable()
+  local bufenter  = [[autocmd BufEnter <buffer> lua require'lean.infoview'.__maybe_autoopen() ]] ..
+                    [[require'lean.infoview'.get_current_infoview():focus_on_current_buffer()]]
+  local bufleave  = [[autocmd BufLeave <buffer> lua require'lean.infoview'.__lean_buffer_left()]]
+  local winclosed = [[autocmd WinClosed <buffer> lua if require'lean.infoview'.get_current_infoview() ]] ..
+                    [[then require'lean.infoview'.get_current_infoview():__clear_win]] ..
+                    [[(tonumber(vim.fn.expand('<afile>')), true) end]]
   -- WinEnter is necessary for the edge case where you have
   -- a file open in a tab with an infoview and move to a
   -- new window in a new tab with that same file but no infoview
-  set_augroup("LeanInfoviewSetFocus", [[
-    autocmd BufEnter <buffer> lua require'lean.infoview'.maybe_autoopen()
-    autocmd BufEnter,WinEnter <buffer> lua if require'lean.infoview'.get_current_infoview()]] ..
-    [[ then require'lean.infoview'.get_current_infoview():focus_on_current_buffer() end
-  ]], 0)
+  local winenter = [[autocmd WinEnter <buffer> lua if require'lean.infoview'.get_current_infoview() ]] ..
+                   [[then require'lean.infoview'.get_current_infoview():focus_on_current_buffer() end]]
+  set_augroup("LeanInfoviewSetFocus", table.concat({bufenter, bufleave, winclosed, winenter}, "\n"), 0)
 end
 
 --- Set whether a new infoview is automatically opened when entering Lean buffers.
 function infoview.set_autoopen(autoopen)
   options.autoopen = autoopen
 end
 
+--- Set whether an infoview is automatically closed when leaving from its last associated Lean file.
+function infoview.set_autoclose(autoclose)
+  options.autoclose = autoclose
+end
+
 --- Open an infoview for the current buffer if it isn't already open.
-function infoview.maybe_autoopen()
+function infoview.__maybe_autoopen()
   local id = get_id()
   if not infoview._by_id[id] then infoview._by_id[id] = Infoview:new(id, options.width, options.autoopen) end
 end

lua/lean/init.lua

@@ -70,8 +70,8 @@ function lean.use_suggested_mappings(buffer_local)
 end
 
 --- Is the current buffer a lean buffer?
-function lean.is_lean_buffer()
-  local filetype = vim.opt.filetype:get()
+function lean.is_lean_buffer(buffer)
+  local filetype = vim.api.nvim_buf_get_option(buffer or 0, "ft")
   return filetype == "lean" or filetype == "lean3"
 end
 

lua/tests/helpers.lua

@@ -17,10 +17,11 @@ local default_config = {
   },
   mappings = false,
   infoview = {
-    enable = false
+    enable = false,
+    autoclose = false
   },
   lsp3 = {
-    enable = false
+    enable = false,
   },
   lsp = {
     enable = false