fix goto_last_window

lua/lean/infoview.lua

@@ -589,24 +589,24 @@ end
 
 ---@return Info
 function Info:new(opts)
-  local pins_element = Element:new {
-    name = 'info',
-    events = {
-      goto_last_window = function()
-        if not self.last_window then
-          return
-        end
-        vim.api.nvim_set_current_win(self.last_window)
-      end,
-    },
-  }
   local new_info = setmetatable({
     pins = {},
     __infoview = opts.infoview,
-    __pins_element = pins_element,
+    __pins_element = Element:new { name = 'info' },
     __diff_pin_element = Element:new { name = 'diff' },
     __win_event_disable = false, -- FIXME: This too is really confusing
   }, self)
+
+  new_info.__pins_element.events = {
+    goto_last_window = function()
+      print(vim.inspect(new_info))
+      if not new_info.last_window then
+        return
+      end
+      vim.api.nvim_set_current_win(new_info.last_window)
+    end,
+  }
+
   new_info.pin = Pin:new {
     id = '1',
     paused = options.autopause,

lua/lean/tui.lua

@@ -8,7 +8,7 @@ local util = require 'lean._util'
 ---keys trigger it (or theoretically mouse events, though we don't do so in
 ---practice at the moment).
 ---
----In gneeral, resist the temptation to add new event types here, as this
+---In general, resist the temptation to add new event types here, as this
 ---entire concept feels slightly like "misdirection" that could be redesigned
 ---at least because it mixes abstraction layers between general events and ones
 ---that are very specific to a particular context (like "going to the last

spec/infoview/jump_spec.lua

@@ -0,0 +1,33 @@
+---@brief [[
+--- Tests for jumping from Lean file to infoview and back
+---@brief ]]
+
+local fixtures = require 'spec.fixtures'
+local helpers = require 'spec.helpers'
+local infoview = require 'lean.infoview'
+
+require('lean').setup {}
+
+describe('infoview jumping', function()
+  local lean_window
+
+  it('jumps from Lean file to infoview', function()
+    assert.is.equal(1, #vim.api.nvim_tabpage_list_wins(0))
+    lean_window = vim.api.nvim_get_current_win()
+
+    vim.cmd('edit! ' .. fixtures.project.some_existing_file)
+    local current_infoview = infoview.get_current_infoview()
+
+    current_infoview:open()
+    -- Both Lean and infoview windows exist
+    assert.windows.are(lean_window, current_infoview.window)
+
+    vim.cmd 'LeanGotoInfoview'
+    assert.current_window.is(current_infoview.window)
+  end)
+
+  it('jumps back from infoview to the associated Lean file', function()
+    helpers.feed '<LocalLeader><Tab>'
+    assert.current_window.is(lean_window)
+  end)
+end)