From 8ceae9875e22e5dee000d8edaa24190525d3029e Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Fri, 23 Jul 2021 18:12:12 -0700
Subject: [PATCH 01/13] Declutter infoview tests.

---
 lua/lean/infoview.lua                      |   4 +-
 lua/tests/helpers.lua                      | 126 +++++++++++++++++++-
 lua/tests/infoview/autoopen_false_spec.lua |   4 +-
 lua/tests/infoview/autoopen_spec.lua       |  24 ++--
 lua/tests/infoview/close_all_spec.lua      |  54 +++++++++
 lua/tests/infoview/run_spec.lua            | 128 ++++++++-------------
 lua/tests/infoview/start_spec.lua          |  29 ++---
 lua/tests/infoview/toggle_spec.lua         |   8 +-
 8 files changed, 254 insertions(+), 123 deletions(-)
 create mode 100644 lua/tests/infoview/close_all_spec.lua

diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua
index f930f5d1..5e7d189c 100644
--- a/lua/lean/infoview.lua
+++ b/lua/lean/infoview.lua
@@ -184,9 +184,11 @@ function Infoview:is_empty()
 end
 
 --- Close all open infoviews (across all tabs).
-function infoview.close_all()
+function infoview.close_all(pre_close_hook, post_close_hook)
   for _, each in pairs(infoview._by_id) do
+    if pre_close_hook then pre_close_hook(each) end
     each:close()
+    if post_close_hook then post_close_hook(each) end
   end
 end
 
diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index b65f1eec..c620b8d4 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -1,4 +1,5 @@
 local assert = require('luassert')
+local infoview = require('lean.infoview')
 
 local lean = require('lean')
 
@@ -98,6 +99,11 @@ end
 --- The number of current windows.
 function helpers.get_num_wins() return #vim.api.nvim_list_wins() end
 
+local last_num_wins
+
+function helpers.set_num_wins() last_num_wins = helpers.get_num_wins() end
+helpers.set_num_wins()
+
 --- Assert about the entire buffer contents.
 local function has_buf_contents(_, arguments)
   local buf = table.concat(vim.api.nvim_buf_get_lines(0, 0, -1, false), '\n')
@@ -116,11 +122,121 @@ local function has_all(_, arguments)
   return true
 end
 
+local prev_buf_max = -1
+local prev_win_max = -1
+local prev_buf
+local prev_win
+
+local function change_infoview(state, _)
+  local this_infoview = infoview.get_current_infoview()
+  local buf = this_infoview.bufnr
+  local win = this_infoview.window
+  local result =
+    ((not buf and not this_infoview.is_open) or (buf and prev_buf ~= buf and this_infoview.is_open
+      and vim.api.nvim_buf_is_valid(buf))) and
+    ((not win and not this_infoview.is_open) or (win and prev_win ~= win and this_infoview.is_open
+      and vim.api.nvim_win_is_valid(win))) and
+    helpers.get_num_wins() == last_num_wins
+  prev_buf = buf
+  prev_win = win
+  state.failure_message = {
+    "Failed to change: ",
+    ("prev_buf: %s, buf: %s, buf valid: %s"):format(vim.inspect(prev_buf), vim.inspect(buf),
+      vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
+    ("prev_win: %s, win: %s, win valid: %s"):format(vim.inspect(prev_win), vim.inspect(win),
+      vim.inspect(win and vim.api.nvim_win_is_valid(win))),
+    "is_open: " .. vim.inspect(this_infoview.is_open),
+    ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
+  }
+
+  return result
+end
+
+local function open_infoview(state, arguments)
+  local result
+  local this_infoview = infoview.get_current_infoview()
+
+  local maintain = arguments[1]
+
+  local failure_message = {}
+
+  if state.mod then
+    local buf = this_infoview.bufnr
+    local win = this_infoview.window
+    vim.list_extend(failure_message,
+    {
+      "Failed to open: ",
+      "maintain: " .. vim.inspect(maintain),
+      ("prev_buf_max: %d, buf: %d, buf valid: %s"):format(prev_buf_max, buf,
+        vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
+      ("prev_win_max: %d, win: %d, win valid: %s"):format(prev_win_max, win,
+        vim.inspect(win and vim.api.nvim_win_is_valid(win))),
+      "is_open: " .. vim.inspect(this_infoview.is_open),
+      ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
+    })
+    if maintain then
+      result = this_infoview.is_open and
+        buf and prev_buf == buf and vim.api.nvim_buf_is_valid(buf) and
+        win and prev_win == win and vim.api.nvim_win_is_valid(win) and
+        helpers.get_num_wins() == last_num_wins
+    else
+      -- make sure this is a brand new buffer/window
+      result = this_infoview.is_open and
+        prev_buf_max < buf and vim.api.nvim_buf_is_valid(buf) and
+        prev_win_max < win and vim.api.nvim_win_is_valid(win) and
+        helpers.get_num_wins() == last_num_wins + 1
+      prev_buf_max = buf
+      prev_win_max = win
+    end
+    prev_buf = buf
+    prev_win = win
+  else
+    vim.list_extend(failure_message,
+    {
+      "Failed to close: ",
+      "maintain: " .. vim.inspect(maintain),
+      ("prev_buf_max: %d, prev_buf: %s, buf valid: %s"):format(prev_buf_max, vim.inspect(prev_buf),
+        prev_buf and vim.inspect(vim.api.nvim_buf_is_valid(prev_buf))),
+      ("prev_win_max: %d, prev_win: %s, win valid: %s"):format(prev_win_max, vim.inspect(prev_win),
+        prev_win and vim.inspect(vim.api.nvim_win_is_valid(prev_win))),
+      "is_open: " .. vim.inspect(this_infoview.is_open),
+      ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
+    })
+    if maintain then
+      result = this_infoview.is_open or helpers.get_num_wins() ~= last_num_wins
+    else
+      -- make sure the previous window was closed
+      result = this_infoview.is_open or
+        vim.api.nvim_buf_is_valid(prev_buf) or
+        vim.api.nvim_win_is_valid(prev_win) or
+        helpers.get_num_wins() ~= last_num_wins - 1
+    end
+    prev_buf = nil
+    prev_win = nil
+  end
+  state.failure_message = table.concat(failure_message, "\n")
+
+  helpers.set_num_wins()
+
+  return result
+end
+
+local function close_win()
+  local result = helpers.get_num_wins() == last_num_wins - 1
+  helpers.set_num_wins()
+  return result
+end
+
+local function new_win()
+  local result = helpers.get_num_wins() == last_num_wins + 1
+  helpers.set_num_wins()
+  return result
+end
+
 assert:register("assertion", "has_all", has_all)
-assert:register(
-  "assertion",
-  "open_infoview",
-  function() return require('lean.infoview').get_current_infoview().is_open end
-)
+assert:register("assertion", "open_infoview", open_infoview)
+assert:register("assertion", "change_infoview", change_infoview)
+assert:register("assertion", "close_win", close_win)
+assert:register("assertion", "new_win", new_win)
 
 return helpers
diff --git a/lua/tests/infoview/autoopen_false_spec.lua b/lua/tests/infoview/autoopen_false_spec.lua
index 5a61c2b1..6d5c7b15 100644
--- a/lua/tests/infoview/autoopen_false_spec.lua
+++ b/lua/tests/infoview/autoopen_false_spec.lua
@@ -5,12 +5,10 @@ require('tests.helpers').setup {
   infoview = { autoopen = false },
 }
 describe('infoview', function()
-  vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-
   it('does not automatically open',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.is_not.open_infoview()
+      assert.is_not.open_infoview(true)
     end)
 
   it('can be opened after no autoopen',
diff --git a/lua/tests/infoview/autoopen_spec.lua b/lua/tests/infoview/autoopen_spec.lua
index e9c10b0e..ef3f9953 100644
--- a/lua/tests/infoview/autoopen_spec.lua
+++ b/lua/tests/infoview/autoopen_spec.lua
@@ -1,12 +1,11 @@
 local infoview = require('lean.infoview')
 local fixtures = require('tests.fixtures')
+local helpers = require('tests.helpers')
 
-require('tests.helpers').setup {
+helpers.setup {
   infoview = { autoopen = true },
 }
 describe('infoview', function()
-  vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-
   it('automatically opens',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
@@ -15,7 +14,9 @@ describe('infoview', function()
 
   it('new tab automatically opens',
     function(_)
-      vim.api.nvim_command('tabedit ' .. fixtures.lean3_project.some_existing_file)
+      vim.api.nvim_command('tabnew')
+      assert.new_win()
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
       assert.open_infoview()
     end)
 
@@ -25,19 +26,21 @@ describe('infoview', function()
       assert.is_not.open_infoview()
     end)
 
-  vim.api.nvim_command("tabnew")
   it('opens automatically after having closen previous infoviews',
   function(_)
+    vim.api.nvim_command("tabnew")
+    assert.new_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
     assert.open_infoview()
   end)
 
-  vim.api.nvim_command("tabnew")
-  infoview.set_autoopen(false)
   it('auto-open disable',
   function(_)
+    vim.api.nvim_command("tabnew")
+    infoview.set_autoopen(false)
+    assert.new_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.is_not.open_infoview()
+    assert.is_not.open_infoview(true)
   end)
 
   it('open after auto-open disable',
@@ -52,10 +55,11 @@ describe('infoview', function()
     assert.is_not.open_infoview()
   end)
 
-  vim.api.nvim_command("tabnew")
-  infoview.set_autoopen(true)
   it('auto-open re-enable',
   function(_)
+    vim.api.nvim_command("tabnew")
+    infoview.set_autoopen(true)
+    assert.new_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
     assert.open_infoview()
   end)
diff --git a/lua/tests/infoview/close_all_spec.lua b/lua/tests/infoview/close_all_spec.lua
new file mode 100644
index 00000000..eba9176b
--- /dev/null
+++ b/lua/tests/infoview/close_all_spec.lua
@@ -0,0 +1,54 @@
+local infoview = require('lean.infoview')
+
+require('tests.helpers').setup {
+  infoview = {},
+}
+describe('infoview', function()
+  it('close_all succeeds',
+  function(_)
+    vim.api.nvim_command("edit temp.lean")
+    infoview.get_current_infoview():open()
+    assert.open_infoview()
+
+    vim.api.nvim_command("tabnew")
+    assert.new_win()
+    vim.api.nvim_command("edit temp.lean")
+    infoview.get_current_infoview():open()
+    assert.open_infoview()
+
+    vim.api.nvim_command("tabnew")
+    assert.new_win()
+    vim.api.nvim_command("edit temp.lean")
+    infoview.get_current_infoview():open()
+    assert.open_infoview()
+    infoview.get_current_infoview():close()
+    assert.is_not.open_infoview()
+
+    vim.api.nvim_command("tabnew")
+    assert.new_win()
+    vim.api.nvim_command("edit temp.lean")
+    infoview.get_current_infoview():open()
+    assert.open_infoview()
+
+
+    local already_closed = false
+    local already_closed_count = 0
+    infoview.close_all(
+    function(info)
+      if info.window ~= vim.api.nvim_get_current_win() then
+        vim.api.nvim_set_current_win(info.window)
+        assert.change_infoview()
+      end
+      if not info.is_open then
+        already_closed = true
+        already_closed_count = already_closed_count + 1
+      end
+    end,
+    function()
+      assert.is_not.open_infoview(already_closed)
+      already_closed = false
+    end
+    )
+    assert.equals(1, already_closed_count)
+  end)
+end)
diff --git a/lua/tests/infoview/run_spec.lua b/lua/tests/infoview/run_spec.lua
index 782707ef..79bce04c 100644
--- a/lua/tests/infoview/run_spec.lua
+++ b/lua/tests/infoview/run_spec.lua
@@ -1,16 +1,10 @@
 local infoview = require('lean.infoview')
-local get_num_wins = require('tests.helpers').get_num_wins
 local fixtures = require('tests.fixtures')
 
 require('tests.helpers').setup {
   infoview = { autoopen = true },
 }
 describe('infoview', function()
-  vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-
-  local win = vim.api.nvim_get_current_win()
-  local infoview_info = infoview.get_current_infoview():open()
-
   local function update_enabled(state, _)
     local cursor_hold = string.find(vim.api.nvim_exec("autocmd CursorHold <buffer>", true), "LeanInfoviewUpdate")
     local cursor_hold_i = string.find(vim.api.nvim_exec("autocmd CursorHoldI <buffer>", true), "LeanInfoviewUpdate")
@@ -25,34 +19,31 @@ describe('infoview', function()
   describe('initial', function()
     it('CursorHold(I) enabled when opened',
     function(_)
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+      assert.open_infoview()
       assert.update_enabled()
     end)
 
     it('closes',
     function(_)
-      local num_wins = get_num_wins()
       infoview.get_current_infoview():close()
-      assert.is_false(vim.api.nvim_win_is_valid(infoview_info.window))
-      assert.is.equal(num_wins - 1, get_num_wins())
       assert.is_not.open_infoview()
     end)
 
     it('remains closed on BufEnter',
     function(_)
-      local num_wins = get_num_wins()
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-      assert.is.equal(num_wins, get_num_wins())
-      assert.is_not.open_infoview()
+      assert.is_not.open_infoview(true)
     end)
 
     it('remains closed on WinEnter',
     function(_)
-      local num_wins = get_num_wins()
       vim.api.nvim_command("split lua/tests/fixtures/example-lean3-project/test.lean")
-      assert.is.equal(num_wins + 1, get_num_wins())
-      assert.is_not.open_infoview()
+      assert.new_win()
+      assert.is_not.open_infoview(true)
+      vim.api.nvim_command("close")
+      assert.close_win()
     end)
-    vim.api.nvim_command("close")
 
     it('CursorHold(I) disabled when closed',
     function(_)
@@ -61,19 +52,14 @@ describe('infoview', function()
 
     it('opens',
     function(_)
-      local num_wins = get_num_wins()
-      infoview_info = infoview.get_current_infoview():open()
-      assert.is_true(vim.api.nvim_win_is_valid(infoview_info.window))
-      assert.is.equal(num_wins + 1, get_num_wins())
+      infoview.get_current_infoview():open()
       assert.open_infoview()
     end)
 
     it('remains open on BufWinEnter',
     function(_)
-      local num_wins = get_num_wins()
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test.lean")
-      assert.is_true(vim.api.nvim_win_is_valid(infoview_info.window))
-      assert.is.equal(num_wins, get_num_wins())
+      assert.open_infoview(true)
     end)
 
     it('CursorHold(I) enabled when re-opened',
@@ -83,128 +69,108 @@ describe('infoview', function()
 
     it('manual quit succeeds and updates internal state',
     function(_)
-      local num_wins = get_num_wins()
-      vim.api.nvim_set_current_win(infoview_info.window)
+      vim.api.nvim_command("wincmd l")
       vim.api.nvim_command("quit")
-      assert.is_false(vim.api.nvim_win_is_valid(infoview_info.window))
-      assert.is.equal(num_wins - 1, get_num_wins())
-      assert.is.equal(win, vim.api.nvim_get_current_win())
       assert.is_not.open_infoview()
     end)
 
     it('manual close succeeds and updates internal state',
     function(_)
-      infoview_info = infoview.get_current_infoview():open()
-      local num_wins = get_num_wins()
-      vim.api.nvim_set_current_win(infoview_info.window)
+      infoview.get_current_infoview():open()
+      assert.open_infoview()
+      vim.api.nvim_command("wincmd l")
       vim.api.nvim_command("close")
-      assert.is_false(vim.api.nvim_win_is_valid(infoview_info.window))
-      assert.is.equal(num_wins - 1, get_num_wins())
-      assert.is.equal(win, vim.api.nvim_get_current_win())
       assert.is_not.open_infoview()
     end)
   end)
 
-  infoview_info = infoview.get_current_infoview():open()
-
-  vim.api.nvim_command("tabedit lua/tests/fixtures/example-lean4-project/Test.lean")
-
-  local new_buf = vim.api.nvim_get_current_buf()
-  local new_win = vim.api.nvim_get_current_win()
-  local new_infoview_info = infoview.get_current_infoview():open()
-
   describe('new tab', function()
     it('closes independently',
     function(_)
-      local num_wins = get_num_wins()
+      infoview.get_current_infoview():open()
+      assert.open_infoview()
+      vim.api.nvim_command("tabnew")
+      assert.new_win()
+      vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test.lean")
+      assert.open_infoview()
       infoview.get_current_infoview():close()
-      assert.is_true(vim.api.nvim_win_is_valid(infoview_info.window))
-      assert.is_false(vim.api.nvim_win_is_valid(new_infoview_info.window))
-      assert.is.equal(num_wins - 1, get_num_wins())
       assert.is_not.open_infoview()
+      assert.is_not.update_enabled()
+      vim.api.nvim_command("tabprevious")
+      assert.change_infoview()
+      assert.open_infoview(true)
     end)
 
     it('CursorHold(I) disabled independently',
     function(_)
-      assert.is_not.update_enabled()
-      vim.api.nvim_set_current_win(win)
       assert.is.update_enabled()
     end)
 
     it('CursorHold(I) updated on BufEnter',
     function(_)
-      vim.api.nvim_set_current_buf(new_buf)
+      vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test.lean")
+      assert.open_infoview(true)
       assert.is.update_enabled()
     end)
 
     it('CursorHold(I) updated on WinEnter',
     function(_)
-      vim.api.nvim_set_current_win(new_win)
+      vim.api.nvim_command("tabnext")
+      assert.change_infoview()
+      assert.is_not.open_infoview(true)
       assert.is_not.update_enabled()
     end)
 
     it('remains closed on BufWinEnter',
     function(_)
-      local num_wins = get_num_wins()
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
-      assert.is.equal(num_wins, get_num_wins())
+      assert.is_not.open_infoview(true)
     end)
 
     it('opens independently',
     function(_)
-      vim.api.nvim_set_current_win(win)
+      vim.api.nvim_command("tabprevious")
+      assert.change_infoview()
       infoview.get_current_infoview():close()
-      vim.api.nvim_set_current_win(new_win)
-      local num_wins = get_num_wins()
-      new_infoview_info = infoview.get_current_infoview():open()
-      assert.is_false(vim.api.nvim_win_is_valid(infoview_info.window))
-      assert.is_true(vim.api.nvim_win_is_valid(new_infoview_info.window))
-      assert.is.equal(num_wins + 1, get_num_wins())
+      assert.is_not.open_infoview()
+      vim.api.nvim_command("tabnext")
+      assert.change_infoview()
+      infoview.get_current_infoview():open()
       assert.open_infoview()
+      vim.api.nvim_command("tabprevious")
+      assert.change_infoview()
+      assert.is_not.open_infoview(true)
+      vim.api.nvim_command("tabnext")
+      assert.change_infoview()
+      assert.open_infoview(true)
     end)
 
     it('remains open on BufWinEnter',
     function(_)
-      local num_wins = get_num_wins()
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
-      assert.is_true(vim.api.nvim_win_is_valid(new_infoview_info.window))
-      assert.is.equal(num_wins, get_num_wins())
+      assert.open_infoview(true)
     end)
 
     it('does not set CursorHold(I) on irrelevant file BufEnter',
     function(_)
       vim.api.nvim_command("edit temp")
+      assert.open_infoview(true)
       assert.is_not.update_enabled()
     end)
 
     it('does not set CursorHold(I) when re-opening on irrelevant file',
     function(_)
       infoview.get_current_infoview():close()
-      new_infoview_info = infoview.get_current_infoview():open()
+      assert.is_not.open_infoview()
+      infoview.get_current_infoview():open()
+      assert.open_infoview()
       assert.is_not.update_enabled()
     end)
 
     it('updates CursorHold(I) on relevant file BufEnter',
     function(_)
-      vim.api.nvim_set_current_buf(new_buf)
+      vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
       assert.update_enabled()
     end)
   end)
-
-  -- TODO
-  it('close_all succeeds',
-  function(_)
-    local num_wins = get_num_wins()
-    infoview.close_all()
-
-    -- should be exactly 1 open at the moment
-    assert.is.equal(num_wins - 1, get_num_wins())
-
-    for _, tab in pairs(vim.api.nvim_list_tabpages()) do
-      vim.api.nvim_set_current_tabpage(tab)
-      if infoview.get_current_infoview() then
-        assert.is_not.open_infoview()
-      end
-    end
-  end)
 end)
diff --git a/lua/tests/infoview/start_spec.lua b/lua/tests/infoview/start_spec.lua
index db21ca74..f37a5f63 100644
--- a/lua/tests/infoview/start_spec.lua
+++ b/lua/tests/infoview/start_spec.lua
@@ -5,18 +5,15 @@ require('tests.helpers').setup { infoview = { autoopen = true } }
 describe('infoview', function()
   describe("startup", function()
     local src_win = vim.api.nvim_get_current_win()
-    vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-    local infoview_info = infoview.get_current_infoview():open()
-
     it('created valid infoview',
       function(_)
-        assert.is_true(vim.api.nvim_win_is_valid(infoview_info.window))
-        assert.is_true(vim.api.nvim_buf_is_valid(infoview_info.bufnr))
+        vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+        assert.open_infoview()
       end)
 
     it('starts with the window position at the top',
       function(_)
-        local cursor = vim.api.nvim_win_get_cursor(infoview_info.window)
+        local cursor = vim.api.nvim_win_get_cursor(infoview.get_current_infoview().window)
         assert.is.same(1, cursor[1])
       end)
 
@@ -26,25 +23,21 @@ describe('infoview', function()
       end)
   end)
 
-  local orig_infoview_info = infoview.get_current_infoview():open()
-
-  vim.api.nvim_command("tabnew")
   describe("new tab", function()
-    local src_win = vim.api.nvim_get_current_win()
-    vim.api.nvim_command('edit ' .. fixtures.lean_project.some_existing_file)
-    local infoview_info = infoview.get_current_infoview():open()
+    local src_win
 
     it('created valid distinct infoview',
       function(_)
-        assert.is_true(vim.api.nvim_win_is_valid(infoview_info.window))
-        assert.is_true(vim.api.nvim_buf_is_valid(infoview_info.bufnr))
-        assert.are_not.equal(orig_infoview_info.bufnr, infoview_info.bufnr)
-        assert.are_not.equal(orig_infoview_info.window, infoview_info.window)
+        vim.api.nvim_command("tabnew")
+        assert.new_win()
+        src_win = vim.api.nvim_get_current_win()
+        vim.api.nvim_command('edit ' .. fixtures.lean_project.some_existing_file)
+        assert.open_infoview()
       end)
 
     it('starts with the window position at the top',
       function(_)
-        local cursor = vim.api.nvim_win_get_cursor(infoview_info.window)
+        local cursor = vim.api.nvim_win_get_cursor(infoview.get_current_infoview().window)
         assert.is.same(1, cursor[1])
       end)
 
@@ -53,6 +46,4 @@ describe('infoview', function()
         assert.is.same(src_win, vim.api.nvim_get_current_win())
       end)
   end)
-
-  infoview.get_current_infoview():close()
 end)
diff --git a/lua/tests/infoview/toggle_spec.lua b/lua/tests/infoview/toggle_spec.lua
index 5c10d5f7..460e0b8d 100644
--- a/lua/tests/infoview/toggle_spec.lua
+++ b/lua/tests/infoview/toggle_spec.lua
@@ -5,25 +5,25 @@ require('tests.helpers').setup {
   infoview = { autoopen = true },
 }
 describe('Infoview.toggle', function()
-  vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-
   it('closes an open infoview', function()
+    vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
     assert.open_infoview()
     infoview.get_current_infoview():toggle()
     assert.is_not.open_infoview()
   end)
 
   it('opens a closed infoview', function()
-    assert.is_not.open_infoview()
     infoview.get_current_infoview():toggle()
     assert.open_infoview()
   end)
 
   it('toggles back and forth', function()
-    assert.open_infoview()
     infoview.get_current_infoview():toggle()
+    assert.is_not.open_infoview()
     infoview.get_current_infoview():toggle()
+    assert.open_infoview()
     infoview.get_current_infoview():toggle()
+    assert.is_not.open_infoview()
     infoview.get_current_infoview():toggle()
     assert.open_infoview()
   end)

From f535de4e6a9cdd3b856d0f58dfb24953ed1e6511 Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Sat, 24 Jul 2021 07:32:00 -0700
Subject: [PATCH 02/13] Check `prev_buf ~= nil` when closing.

---
 lua/tests/helpers.lua | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index c620b8d4..f6f5a452 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -207,8 +207,8 @@ local function open_infoview(state, arguments)
     else
       -- make sure the previous window was closed
       result = this_infoview.is_open or
-        vim.api.nvim_buf_is_valid(prev_buf) or
-        vim.api.nvim_win_is_valid(prev_win) or
+        (not prev_buf) or vim.api.nvim_buf_is_valid(prev_buf) or
+        (not prev_win) or vim.api.nvim_win_is_valid(prev_win) or
         helpers.get_num_wins() ~= last_num_wins - 1
     end
     prev_buf = nil

From 45ed26e612a661fcc8c9cfae29da5ec1383abb04 Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Sat, 24 Jul 2021 07:56:09 -0700
Subject: [PATCH 03/13] Make `set_num_wins` local to `helpers.lua`.

---
 lua/tests/helpers.lua | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index f6f5a452..cd529311 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -101,8 +101,8 @@ function helpers.get_num_wins() return #vim.api.nvim_list_wins() end
 
 local last_num_wins
 
-function helpers.set_num_wins() last_num_wins = helpers.get_num_wins() end
-helpers.set_num_wins()
+local function set_num_wins() last_num_wins = helpers.get_num_wins() end
+set_num_wins()
 
 --- Assert about the entire buffer contents.
 local function has_buf_contents(_, arguments)
@@ -216,20 +216,20 @@ local function open_infoview(state, arguments)
   end
   state.failure_message = table.concat(failure_message, "\n")
 
-  helpers.set_num_wins()
+  set_num_wins()
 
   return result
 end
 
 local function close_win()
   local result = helpers.get_num_wins() == last_num_wins - 1
-  helpers.set_num_wins()
+  set_num_wins()
   return result
 end
 
 local function new_win()
   local result = helpers.get_num_wins() == last_num_wins + 1
-  helpers.set_num_wins()
+  set_num_wins()
   return result
 end
 

From 376fb5616f2aa3daab336c7b241c3d2b403cb11f Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Sat, 24 Jul 2021 18:59:21 -0700
Subject: [PATCH 04/13] Clean up `is_open` logic.

---
 lua/tests/helpers.lua                      | 34 +++++++++++++---------
 lua/tests/infoview/autoopen_false_spec.lua |  2 +-
 lua/tests/infoview/autoopen_spec.lua       |  2 +-
 3 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index cd529311..c16094c3 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -160,9 +160,9 @@ local function open_infoview(state, arguments)
 
   local failure_message = {}
 
+  local buf = this_infoview.bufnr
+  local win = this_infoview.window
   if state.mod then
-    local buf = this_infoview.bufnr
-    local win = this_infoview.window
     vim.list_extend(failure_message,
     {
       "Failed to open: ",
@@ -188,32 +188,38 @@ local function open_infoview(state, arguments)
       prev_buf_max = buf
       prev_win_max = win
     end
-    prev_buf = buf
-    prev_win = win
   else
     vim.list_extend(failure_message,
     {
       "Failed to close: ",
       "maintain: " .. vim.inspect(maintain),
-      ("prev_buf_max: %d, prev_buf: %s, buf valid: %s"):format(prev_buf_max, vim.inspect(prev_buf),
+      ("buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(buf), vim.inspect(prev_buf),
         prev_buf and vim.inspect(vim.api.nvim_buf_is_valid(prev_buf))),
-      ("prev_win_max: %d, prev_win: %s, win valid: %s"):format(prev_win_max, vim.inspect(prev_win),
+      ("win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(win), vim.inspect(prev_win),
         prev_win and vim.inspect(vim.api.nvim_win_is_valid(prev_win))),
       "is_open: " .. vim.inspect(this_infoview.is_open),
       ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
     })
     if maintain then
-      result = this_infoview.is_open or helpers.get_num_wins() ~= last_num_wins
+      result = buf or win or prev_win or prev_buf or this_infoview.is_open
+        or helpers.get_num_wins() ~= last_num_wins
     else
-      -- make sure the previous window was closed
-      result = this_infoview.is_open or
-        (not prev_buf) or vim.api.nvim_buf_is_valid(prev_buf) or
-        (not prev_win) or vim.api.nvim_win_is_valid(prev_win) or
-        helpers.get_num_wins() ~= last_num_wins - 1
+      local unopened = arguments[2]
+      if unopened then
+        -- if not previously opened, we don't care about prev_win or prev_buf being accurate
+        result = buf or win or this_infoview.is_open
+          or helpers.get_num_wins() ~= last_num_wins
+      else
+        -- make sure the previous window was closed
+        result = this_infoview.is_open or buf or win or
+          (not prev_buf) or vim.api.nvim_buf_is_valid(prev_buf) or
+          (not prev_win) or vim.api.nvim_win_is_valid(prev_win) or
+          helpers.get_num_wins() ~= last_num_wins - 1
+      end
     end
-    prev_buf = nil
-    prev_win = nil
   end
+  prev_buf = buf
+  prev_win = win
   state.failure_message = table.concat(failure_message, "\n")
 
   set_num_wins()
diff --git a/lua/tests/infoview/autoopen_false_spec.lua b/lua/tests/infoview/autoopen_false_spec.lua
index 6d5c7b15..2a91fdac 100644
--- a/lua/tests/infoview/autoopen_false_spec.lua
+++ b/lua/tests/infoview/autoopen_false_spec.lua
@@ -8,7 +8,7 @@ describe('infoview', function()
   it('does not automatically open',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.is_not.open_infoview(true)
+      assert.is_not.open_infoview(false, true)
     end)
 
   it('can be opened after no autoopen',
diff --git a/lua/tests/infoview/autoopen_spec.lua b/lua/tests/infoview/autoopen_spec.lua
index ef3f9953..7583ec99 100644
--- a/lua/tests/infoview/autoopen_spec.lua
+++ b/lua/tests/infoview/autoopen_spec.lua
@@ -40,7 +40,7 @@ describe('infoview', function()
     infoview.set_autoopen(false)
     assert.new_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.is_not.open_infoview(true)
+    assert.is_not.open_infoview(false, true)
   end)
 
   it('open after auto-open disable',

From c7c2e73e922eaa4aeb03b15b35032d7711d1d817 Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Sat, 24 Jul 2021 19:17:21 -0700
Subject: [PATCH 05/13] Improve failure messages.

---
 lua/tests/helpers.lua | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index c16094c3..3a65db5d 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -139,7 +139,7 @@ local function change_infoview(state, _)
     helpers.get_num_wins() == last_num_wins
   prev_buf = buf
   prev_win = win
-  state.failure_message = {
+  state.failure_message = table.concat({
     "Failed to change: ",
     ("prev_buf: %s, buf: %s, buf valid: %s"):format(vim.inspect(prev_buf), vim.inspect(buf),
       vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
@@ -147,7 +147,7 @@ local function change_infoview(state, _)
       vim.inspect(win and vim.api.nvim_win_is_valid(win))),
     "is_open: " .. vim.inspect(this_infoview.is_open),
     ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
-  }
+  }, "\n")
 
   return result
 end
@@ -167,9 +167,11 @@ local function open_infoview(state, arguments)
     {
       "Failed to open: ",
       "maintain: " .. vim.inspect(maintain),
-      ("prev_buf_max: %d, buf: %d, buf valid: %s"):format(prev_buf_max, buf,
+      ("prev_buf_max: %s, buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(prev_buf_max),
+        vim.inspect(buf), vim.inspect(prev_buf),
         vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
-      ("prev_win_max: %d, win: %d, win valid: %s"):format(prev_win_max, win,
+      ("prev_win_max: %s, win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(prev_win_max),
+        vim.inspect(win), vim.inspect(prev_win),
         vim.inspect(win and vim.api.nvim_win_is_valid(win))),
       "is_open: " .. vim.inspect(this_infoview.is_open),
       ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
@@ -205,6 +207,7 @@ local function open_infoview(state, arguments)
         or helpers.get_num_wins() ~= last_num_wins
     else
       local unopened = arguments[2]
+      vim.list_extend(failure_message, {"unopened: " .. vim.inspect(unopened)})
       if unopened then
         -- if not previously opened, we don't care about prev_win or prev_buf being accurate
         result = buf or win or this_infoview.is_open

From 74e5bc75cf73434ce4551c656f02d8e428e415c5 Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Sun, 25 Jul 2021 06:13:05 -0700
Subject: [PATCH 06/13] Readablility improvements.

---
 lua/tests/helpers.lua                      | 19 ++++++++-
 lua/tests/infoview/autoopen_false_spec.lua |  4 +-
 lua/tests/infoview/autoopen_spec.lua       | 16 ++++----
 lua/tests/infoview/close_all_spec.lua      | 12 +++---
 lua/tests/infoview/run_spec.lua            | 48 +++++++++++-----------
 lua/tests/infoview/start_spec.lua          |  4 +-
 lua/tests/infoview/toggle_spec.lua         | 14 +++----
 7 files changed, 66 insertions(+), 51 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index 3a65db5d..7f337ea4 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -152,7 +152,7 @@ local function change_infoview(state, _)
   return result
 end
 
-local function open_infoview(state, arguments)
+local function opened_infoview(state, arguments)
   local result
   local this_infoview = infoview.get_current_infoview()
 
@@ -243,7 +243,22 @@ local function new_win()
 end
 
 assert:register("assertion", "has_all", has_all)
-assert:register("assertion", "open_infoview", open_infoview)
+assert:register("assertion", "opened_infoview", opened_infoview)
+assert:register("assertion", "opened_infoview_kept", function(state, _)
+  return opened_infoview(state, {true, false})
+end)
+assert:register("assertion", "closed_infoview", function(state, _)
+  state.mod = false
+  return opened_infoview(state, {false, false})
+end)
+assert:register("assertion", "closed_infoview_kept", function(state, _)
+  state.mod = false
+  return opened_infoview(state, {true, false})
+end)
+assert:register("assertion", "unopened_infoview", function(state, _)
+  state.mod = false
+  return opened_infoview(state, {false, true})
+end)
 assert:register("assertion", "change_infoview", change_infoview)
 assert:register("assertion", "close_win", close_win)
 assert:register("assertion", "new_win", new_win)
diff --git a/lua/tests/infoview/autoopen_false_spec.lua b/lua/tests/infoview/autoopen_false_spec.lua
index 2a91fdac..2adcc018 100644
--- a/lua/tests/infoview/autoopen_false_spec.lua
+++ b/lua/tests/infoview/autoopen_false_spec.lua
@@ -8,12 +8,12 @@ describe('infoview', function()
   it('does not automatically open',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.is_not.open_infoview(false, true)
+      assert.unopened_infoview()
     end)
 
   it('can be opened after no autoopen',
     function(_)
       infoview.get_current_infoview():open()
-      assert.open_infoview()
+      assert.opened_infoview()
     end)
 end)
diff --git a/lua/tests/infoview/autoopen_spec.lua b/lua/tests/infoview/autoopen_spec.lua
index 7583ec99..f16d0280 100644
--- a/lua/tests/infoview/autoopen_spec.lua
+++ b/lua/tests/infoview/autoopen_spec.lua
@@ -9,7 +9,7 @@ describe('infoview', function()
   it('automatically opens',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.open_infoview()
+      assert.opened_infoview()
     end)
 
   it('new tab automatically opens',
@@ -17,13 +17,13 @@ describe('infoview', function()
       vim.api.nvim_command('tabnew')
       assert.new_win()
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.open_infoview()
+      assert.opened_infoview()
     end)
 
   it('can be closed after autoopen',
     function(_)
       infoview.get_current_infoview():close()
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
     end)
 
   it('opens automatically after having closen previous infoviews',
@@ -31,7 +31,7 @@ describe('infoview', function()
     vim.api.nvim_command("tabnew")
     assert.new_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 
   it('auto-open disable',
@@ -40,19 +40,19 @@ describe('infoview', function()
     infoview.set_autoopen(false)
     assert.new_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.is_not.open_infoview(false, true)
+    assert.unopened_infoview()
   end)
 
   it('open after auto-open disable',
   function(_)
     infoview.get_current_infoview():open()
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 
   it('close after auto-open disable',
   function(_)
     infoview.get_current_infoview():close()
-    assert.is_not.open_infoview()
+    assert.closed_infoview()
   end)
 
   it('auto-open re-enable',
@@ -61,7 +61,7 @@ describe('infoview', function()
     infoview.set_autoopen(true)
     assert.new_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 
   it('no auto-open for irrelevant file',
diff --git a/lua/tests/infoview/close_all_spec.lua b/lua/tests/infoview/close_all_spec.lua
index eba9176b..0a3737c7 100644
--- a/lua/tests/infoview/close_all_spec.lua
+++ b/lua/tests/infoview/close_all_spec.lua
@@ -8,27 +8,27 @@ describe('infoview', function()
   function(_)
     vim.api.nvim_command("edit temp.lean")
     infoview.get_current_infoview():open()
-    assert.open_infoview()
+    assert.opened_infoview()
 
     vim.api.nvim_command("tabnew")
     assert.new_win()
     vim.api.nvim_command("edit temp.lean")
     infoview.get_current_infoview():open()
-    assert.open_infoview()
+    assert.opened_infoview()
 
     vim.api.nvim_command("tabnew")
     assert.new_win()
     vim.api.nvim_command("edit temp.lean")
     infoview.get_current_infoview():open()
-    assert.open_infoview()
+    assert.opened_infoview()
     infoview.get_current_infoview():close()
-    assert.is_not.open_infoview()
+    assert.closed_infoview()
 
     vim.api.nvim_command("tabnew")
     assert.new_win()
     vim.api.nvim_command("edit temp.lean")
     infoview.get_current_infoview():open()
-    assert.open_infoview()
+    assert.opened_infoview()
 
 
     local already_closed = false
@@ -45,7 +45,7 @@ describe('infoview', function()
       end
     end,
     function()
-      assert.is_not.open_infoview(already_closed)
+      assert.is_not.opened_infoview(already_closed)
       already_closed = false
     end
     )
diff --git a/lua/tests/infoview/run_spec.lua b/lua/tests/infoview/run_spec.lua
index 79bce04c..51edc653 100644
--- a/lua/tests/infoview/run_spec.lua
+++ b/lua/tests/infoview/run_spec.lua
@@ -20,27 +20,27 @@ describe('infoview', function()
     it('CursorHold(I) enabled when opened',
     function(_)
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-      assert.open_infoview()
+      assert.opened_infoview()
       assert.update_enabled()
     end)
 
     it('closes',
     function(_)
       infoview.get_current_infoview():close()
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
     end)
 
     it('remains closed on BufEnter',
     function(_)
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
-      assert.is_not.open_infoview(true)
+      assert.closed_infoview_kept()
     end)
 
     it('remains closed on WinEnter',
     function(_)
       vim.api.nvim_command("split lua/tests/fixtures/example-lean3-project/test.lean")
       assert.new_win()
-      assert.is_not.open_infoview(true)
+      assert.closed_infoview_kept()
       vim.api.nvim_command("close")
       assert.close_win()
     end)
@@ -53,13 +53,13 @@ describe('infoview', function()
     it('opens',
     function(_)
       infoview.get_current_infoview():open()
-      assert.open_infoview()
+      assert.opened_infoview()
     end)
 
     it('remains open on BufWinEnter',
     function(_)
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test.lean")
-      assert.open_infoview(true)
+      assert.opened_infoview_kept()
     end)
 
     it('CursorHold(I) enabled when re-opened',
@@ -71,16 +71,16 @@ describe('infoview', function()
     function(_)
       vim.api.nvim_command("wincmd l")
       vim.api.nvim_command("quit")
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
     end)
 
     it('manual close succeeds and updates internal state',
     function(_)
       infoview.get_current_infoview():open()
-      assert.open_infoview()
+      assert.opened_infoview()
       vim.api.nvim_command("wincmd l")
       vim.api.nvim_command("close")
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
     end)
   end)
 
@@ -88,17 +88,17 @@ describe('infoview', function()
     it('closes independently',
     function(_)
       infoview.get_current_infoview():open()
-      assert.open_infoview()
+      assert.opened_infoview()
       vim.api.nvim_command("tabnew")
       assert.new_win()
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test.lean")
-      assert.open_infoview()
+      assert.opened_infoview()
       infoview.get_current_infoview():close()
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
       assert.is_not.update_enabled()
       vim.api.nvim_command("tabprevious")
       assert.change_infoview()
-      assert.open_infoview(true)
+      assert.opened_infoview_kept()
     end)
 
     it('CursorHold(I) disabled independently',
@@ -109,7 +109,7 @@ describe('infoview', function()
     it('CursorHold(I) updated on BufEnter',
     function(_)
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test.lean")
-      assert.open_infoview(true)
+      assert.opened_infoview_kept()
       assert.is.update_enabled()
     end)
 
@@ -117,14 +117,14 @@ describe('infoview', function()
     function(_)
       vim.api.nvim_command("tabnext")
       assert.change_infoview()
-      assert.is_not.open_infoview(true)
+      assert.closed_infoview_kept()
       assert.is_not.update_enabled()
     end)
 
     it('remains closed on BufWinEnter',
     function(_)
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
-      assert.is_not.open_infoview(true)
+      assert.closed_infoview_kept()
     end)
 
     it('opens independently',
@@ -132,38 +132,38 @@ describe('infoview', function()
       vim.api.nvim_command("tabprevious")
       assert.change_infoview()
       infoview.get_current_infoview():close()
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
       vim.api.nvim_command("tabnext")
       assert.change_infoview()
       infoview.get_current_infoview():open()
-      assert.open_infoview()
+      assert.opened_infoview()
       vim.api.nvim_command("tabprevious")
       assert.change_infoview()
-      assert.is_not.open_infoview(true)
+      assert.closed_infoview_kept()
       vim.api.nvim_command("tabnext")
       assert.change_infoview()
-      assert.open_infoview(true)
+      assert.opened_infoview_kept()
     end)
 
     it('remains open on BufWinEnter',
     function(_)
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
-      assert.open_infoview(true)
+      assert.opened_infoview_kept()
     end)
 
     it('does not set CursorHold(I) on irrelevant file BufEnter',
     function(_)
       vim.api.nvim_command("edit temp")
-      assert.open_infoview(true)
+      assert.opened_infoview_kept()
       assert.is_not.update_enabled()
     end)
 
     it('does not set CursorHold(I) when re-opening on irrelevant file',
     function(_)
       infoview.get_current_infoview():close()
-      assert.is_not.open_infoview()
+      assert.closed_infoview()
       infoview.get_current_infoview():open()
-      assert.open_infoview()
+      assert.opened_infoview()
       assert.is_not.update_enabled()
     end)
 
diff --git a/lua/tests/infoview/start_spec.lua b/lua/tests/infoview/start_spec.lua
index f37a5f63..3443560d 100644
--- a/lua/tests/infoview/start_spec.lua
+++ b/lua/tests/infoview/start_spec.lua
@@ -8,7 +8,7 @@ describe('infoview', function()
     it('created valid infoview',
       function(_)
         vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-        assert.open_infoview()
+        assert.opened_infoview()
       end)
 
     it('starts with the window position at the top',
@@ -32,7 +32,7 @@ describe('infoview', function()
         assert.new_win()
         src_win = vim.api.nvim_get_current_win()
         vim.api.nvim_command('edit ' .. fixtures.lean_project.some_existing_file)
-        assert.open_infoview()
+        assert.opened_infoview()
       end)
 
     it('starts with the window position at the top',
diff --git a/lua/tests/infoview/toggle_spec.lua b/lua/tests/infoview/toggle_spec.lua
index 460e0b8d..d3a64ae4 100644
--- a/lua/tests/infoview/toggle_spec.lua
+++ b/lua/tests/infoview/toggle_spec.lua
@@ -7,24 +7,24 @@ require('tests.helpers').setup {
 describe('Infoview.toggle', function()
   it('closes an open infoview', function()
     vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
-    assert.open_infoview()
+    assert.opened_infoview()
     infoview.get_current_infoview():toggle()
-    assert.is_not.open_infoview()
+    assert.closed_infoview()
   end)
 
   it('opens a closed infoview', function()
     infoview.get_current_infoview():toggle()
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 
   it('toggles back and forth', function()
     infoview.get_current_infoview():toggle()
-    assert.is_not.open_infoview()
+    assert.closed_infoview()
     infoview.get_current_infoview():toggle()
-    assert.open_infoview()
+    assert.opened_infoview()
     infoview.get_current_infoview():toggle()
-    assert.is_not.open_infoview()
+    assert.closed_infoview()
     infoview.get_current_infoview():toggle()
-    assert.open_infoview()
+    assert.opened_infoview()
   end)
 end)

From cc4e5d42d673a156bc6480062325e90c8f257bc6 Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Sun, 25 Jul 2021 09:52:48 -0700
Subject: [PATCH 07/13] Separate `opened_infoview` and `closed_infoview`.

---
 lua/tests/helpers.lua | 154 +++++++++++++++++++++++-------------------
 1 file changed, 85 insertions(+), 69 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index 7f337ea4..7d111008 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -152,80 +152,85 @@ local function change_infoview(state, _)
   return result
 end
 
-local function opened_infoview(state, arguments)
+local function opened_infoview(failure_message, maintain)
   local result
   local this_infoview = infoview.get_current_infoview()
 
-  local maintain = arguments[1]
+  local buf = this_infoview.bufnr
+  local win = this_infoview.window
 
-  local failure_message = {}
+  vim.list_extend(failure_message,
+  {
+    "Failed to open: ",
+    "maintain: " .. vim.inspect(maintain),
+    ("prev_buf_max: %s, buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(prev_buf_max),
+      vim.inspect(buf), vim.inspect(prev_buf),
+      vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
+    ("prev_win_max: %s, win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(prev_win_max),
+      vim.inspect(win), vim.inspect(prev_win),
+      vim.inspect(win and vim.api.nvim_win_is_valid(win))),
+    "is_open: " .. vim.inspect(this_infoview.is_open),
+    ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
+  })
+  if maintain then
+    result = this_infoview.is_open and
+      buf and prev_buf == buf and vim.api.nvim_buf_is_valid(buf) and
+      win and prev_win == win and vim.api.nvim_win_is_valid(win) and
+      helpers.get_num_wins() == last_num_wins
+  else
+    -- make sure this is a brand new buffer/window
+    result = this_infoview.is_open and
+      prev_buf_max < buf and vim.api.nvim_buf_is_valid(buf) and
+      prev_win_max < win and vim.api.nvim_win_is_valid(win) and
+      helpers.get_num_wins() == last_num_wins + 1
+    prev_buf_max = buf
+    prev_win_max = win
+  end
+
+  prev_buf = buf
+  prev_win = win
+
+  return result
+end
+
+local function closed_infoview(failure_message, maintain, unopened)
+  local result
+  local this_infoview = infoview.get_current_infoview()
 
   local buf = this_infoview.bufnr
   local win = this_infoview.window
-  if state.mod then
-    vim.list_extend(failure_message,
-    {
-      "Failed to open: ",
-      "maintain: " .. vim.inspect(maintain),
-      ("prev_buf_max: %s, buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(prev_buf_max),
-        vim.inspect(buf), vim.inspect(prev_buf),
-        vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
-      ("prev_win_max: %s, win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(prev_win_max),
-        vim.inspect(win), vim.inspect(prev_win),
-        vim.inspect(win and vim.api.nvim_win_is_valid(win))),
-      "is_open: " .. vim.inspect(this_infoview.is_open),
-      ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
-    })
-    if maintain then
-      result = this_infoview.is_open and
-        buf and prev_buf == buf and vim.api.nvim_buf_is_valid(buf) and
-        win and prev_win == win and vim.api.nvim_win_is_valid(win) and
-        helpers.get_num_wins() == last_num_wins
-    else
-      -- make sure this is a brand new buffer/window
-      result = this_infoview.is_open and
-        prev_buf_max < buf and vim.api.nvim_buf_is_valid(buf) and
-        prev_win_max < win and vim.api.nvim_win_is_valid(win) and
-        helpers.get_num_wins() == last_num_wins + 1
-      prev_buf_max = buf
-      prev_win_max = win
-    end
+
+  vim.list_extend(failure_message,
+  {
+    "Failed to close: ",
+    "maintain: " .. vim.inspect(maintain),
+    ("buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(buf), vim.inspect(prev_buf),
+      prev_buf and vim.inspect(vim.api.nvim_buf_is_valid(prev_buf))),
+    ("win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(win), vim.inspect(prev_win),
+      prev_win and vim.inspect(vim.api.nvim_win_is_valid(prev_win))),
+    "is_open: " .. vim.inspect(this_infoview.is_open),
+    ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
+  })
+  if maintain then
+    result = not buf and not win and not prev_win and not prev_buf and not this_infoview.is_open
+      and helpers.get_num_wins() == last_num_wins
   else
-    vim.list_extend(failure_message,
-    {
-      "Failed to close: ",
-      "maintain: " .. vim.inspect(maintain),
-      ("buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(buf), vim.inspect(prev_buf),
-        prev_buf and vim.inspect(vim.api.nvim_buf_is_valid(prev_buf))),
-      ("win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(win), vim.inspect(prev_win),
-        prev_win and vim.inspect(vim.api.nvim_win_is_valid(prev_win))),
-      "is_open: " .. vim.inspect(this_infoview.is_open),
-      ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
-    })
-    if maintain then
-      result = buf or win or prev_win or prev_buf or this_infoview.is_open
-        or helpers.get_num_wins() ~= last_num_wins
+    vim.list_extend(failure_message, {"unopened: " .. vim.inspect(unopened)})
+    if unopened then
+      -- if not previously opened, we don't care about prev_win or prev_buf being accurate
+      result = not buf and not win and not this_infoview.is_open
+        and helpers.get_num_wins() == last_num_wins
     else
-      local unopened = arguments[2]
-      vim.list_extend(failure_message, {"unopened: " .. vim.inspect(unopened)})
-      if unopened then
-        -- if not previously opened, we don't care about prev_win or prev_buf being accurate
-        result = buf or win or this_infoview.is_open
-          or helpers.get_num_wins() ~= last_num_wins
-      else
-        -- make sure the previous window was closed
-        result = this_infoview.is_open or buf or win or
-          (not prev_buf) or vim.api.nvim_buf_is_valid(prev_buf) or
-          (not prev_win) or vim.api.nvim_win_is_valid(prev_win) or
-          helpers.get_num_wins() ~= last_num_wins - 1
-      end
+      -- make sure the previous window was closed
+      result = not this_infoview.is_open and not buf and not win and
+        prev_buf and not vim.api.nvim_buf_is_valid(prev_buf) and
+        prev_win and not vim.api.nvim_win_is_valid(prev_win) and
+        helpers.get_num_wins() == last_num_wins - 1
     end
   end
+
   prev_buf = buf
   prev_win = win
-  state.failure_message = table.concat(failure_message, "\n")
-
-  set_num_wins()
 
   return result
 end
@@ -242,22 +247,33 @@ local function new_win()
   return result
 end
 
+local function infoview_check(state, checker, ...)
+  local failure_message = {}
+
+  local result = checker(failure_message, ...)
+
+  state.failure_message = table.concat(failure_message, "\n")
+
+  set_num_wins()
+
+  return result
+end
+
 assert:register("assertion", "has_all", has_all)
-assert:register("assertion", "opened_infoview", opened_infoview)
+assert:register("assertion", "opened_infoview", function(state, _)
+  return infoview_check(state, opened_infoview, false)
+end)
 assert:register("assertion", "opened_infoview_kept", function(state, _)
-  return opened_infoview(state, {true, false})
+  return infoview_check(state, opened_infoview, true)
 end)
 assert:register("assertion", "closed_infoview", function(state, _)
-  state.mod = false
-  return opened_infoview(state, {false, false})
+  return infoview_check(state, closed_infoview, false, false)
 end)
 assert:register("assertion", "closed_infoview_kept", function(state, _)
-  state.mod = false
-  return opened_infoview(state, {true, false})
+  return infoview_check(state, closed_infoview, true, false)
 end)
 assert:register("assertion", "unopened_infoview", function(state, _)
-  state.mod = false
-  return opened_infoview(state, {false, true})
+  return infoview_check(state, closed_infoview, false, true)
 end)
 assert:register("assertion", "change_infoview", change_infoview)
 assert:register("assertion", "close_win", close_win)

From 20ce93335e86970a8759812a8d0cd4a499ee80dd Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Sun, 25 Jul 2021 11:21:06 -0700
Subject: [PATCH 08/13] Make testing more general/complete.

---
 lua/lean/infoview.lua                 |   4 +-
 lua/tests/helpers.lua                 | 327 +++++++++++++++-----------
 lua/tests/infoview/autoopen_spec.lua  |   8 +-
 lua/tests/infoview/close_all_spec.lua | 101 ++++----
 lua/tests/infoview/run_spec.lua       |  14 +-
 lua/tests/infoview/start_spec.lua     |   2 +-
 6 files changed, 258 insertions(+), 198 deletions(-)

diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua
index 5e7d189c..f930f5d1 100644
--- a/lua/lean/infoview.lua
+++ b/lua/lean/infoview.lua
@@ -184,11 +184,9 @@ function Infoview:is_empty()
 end
 
 --- Close all open infoviews (across all tabs).
-function infoview.close_all(pre_close_hook, post_close_hook)
+function infoview.close_all()
   for _, each in pairs(infoview._by_id) do
-    if pre_close_hook then pre_close_hook(each) end
     each:close()
-    if post_close_hook then post_close_hook(each) end
   end
 end
 
diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index 7d111008..3ffff2cc 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -96,14 +96,6 @@ function helpers.wait_for_line_diagnostics()
   assert.message("Waited for line diagnostics but none came.").True(succeeded)
 end
 
---- The number of current windows.
-function helpers.get_num_wins() return #vim.api.nvim_list_wins() end
-
-local last_num_wins
-
-local function set_num_wins() last_num_wins = helpers.get_num_wins() end
-set_num_wins()
-
 --- Assert about the entire buffer contents.
 local function has_buf_contents(_, arguments)
   local buf = table.concat(vim.api.nvim_buf_get_lines(0, 0, -1, false), '\n')
@@ -122,161 +114,226 @@ local function has_all(_, arguments)
   return true
 end
 
-local prev_buf_max = -1
-local prev_win_max = -1
-local prev_buf
-local prev_win
-
-local function change_infoview(state, _)
-  local this_infoview = infoview.get_current_infoview()
-  local buf = this_infoview.bufnr
-  local win = this_infoview.window
-  local result =
-    ((not buf and not this_infoview.is_open) or (buf and prev_buf ~= buf and this_infoview.is_open
-      and vim.api.nvim_buf_is_valid(buf))) and
-    ((not win and not this_infoview.is_open) or (win and prev_win ~= win and this_infoview.is_open
-      and vim.api.nvim_win_is_valid(win))) and
-    helpers.get_num_wins() == last_num_wins
-  prev_buf = buf
-  prev_win = win
-  state.failure_message = table.concat({
-    "Failed to change: ",
-    ("prev_buf: %s, buf: %s, buf valid: %s"):format(vim.inspect(prev_buf), vim.inspect(buf),
-      vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
-    ("prev_win: %s, win: %s, win valid: %s"):format(vim.inspect(prev_win), vim.inspect(win),
-      vim.inspect(win and vim.api.nvim_win_is_valid(win))),
-    "is_open: " .. vim.inspect(this_infoview.is_open),
-    ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
-  }, "\n")
-
-  return result
+--- The number of current windows.
+function helpers.get_num_wins() return #vim.api.nvim_list_wins() end
+
+local last_wins = {}
+local last_win = nil
+local last_win_max = -1
+
+local function get_wins()
+  local wins = {}
+  for _, win in pairs(vim.api.nvim_list_wins()) do
+    wins[win] = true
+  end
+
+  return wins
 end
 
-local function opened_infoview(failure_message, maintain)
-  local result
-  local this_infoview = infoview.get_current_infoview()
-
-  local buf = this_infoview.bufnr
-  local win = this_infoview.window
-
-  vim.list_extend(failure_message,
-  {
-    "Failed to open: ",
-    "maintain: " .. vim.inspect(maintain),
-    ("prev_buf_max: %s, buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(prev_buf_max),
-      vim.inspect(buf), vim.inspect(prev_buf),
-      vim.inspect(buf and vim.api.nvim_buf_is_valid(buf))),
-    ("prev_win_max: %s, win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(prev_win_max),
-      vim.inspect(win), vim.inspect(prev_win),
-      vim.inspect(win and vim.api.nvim_win_is_valid(win))),
-    "is_open: " .. vim.inspect(this_infoview.is_open),
-    ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
-  })
-  if maintain then
-    result = this_infoview.is_open and
-      buf and prev_buf == buf and vim.api.nvim_buf_is_valid(buf) and
-      win and prev_win == win and vim.api.nvim_win_is_valid(win) and
-      helpers.get_num_wins() == last_num_wins
-  else
-    -- make sure this is a brand new buffer/window
-    result = this_infoview.is_open and
-      prev_buf_max < buf and vim.api.nvim_buf_is_valid(buf) and
-      prev_win_max < win and vim.api.nvim_win_is_valid(win) and
-      helpers.get_num_wins() == last_num_wins + 1
-    prev_buf_max = buf
-    prev_win_max = win
+local function update_wins(_, arguments)
+  -- inductive hypothesis: last_wins is accurate to immediately before creating/closing any of the given windows
+  local expected_wins = vim.deepcopy(last_wins)
+
+  local opened_wins = arguments[1] or {}
+  local closed_wins = arguments[2] or {}
+
+  -- for ensuring no collisions
+  local opened_win_set = {}
+
+  for _, opened_win in pairs(opened_wins) do
+    -- should be an actual window
+    assert.is_truthy(vim.api.nvim_win_is_valid(opened_win))
+
+    -- should be brand new
+    assert.is_truthy(opened_win > last_win_max)
+    assert.is_falsy(opened_win_set[opened_win])
+
+    expected_wins[opened_win] = true
+    opened_win_set[opened_win] = true
+  end
+
+  for _, closed_win in pairs(closed_wins) do
+    -- should not be a window
+    assert.is_falsy(vim.api.nvim_win_is_valid(closed_win))
+
+    -- should have previously existed (should not pass a random previously/never closed window)
+    assert.is_truthy(expected_wins[closed_win])
+
+    expected_wins[closed_win] = nil
+  end
+
+  assert.message("expected: " .. vim.inspect(expected_wins) .. "\n got: " .. vim.inspect(get_wins())).is_truthy(
+    vim.deep_equal(expected_wins, get_wins()))
+
+  for _, opened_win in pairs(opened_wins) do
+    if opened_win > last_win_max then last_win_max = opened_win end
   end
 
-  prev_buf = buf
-  prev_win = win
+  -- maintain IH
+  last_wins = get_wins()
 
-  return result
+  -- also maintain IH for closed_win
+  last_win = vim.api.nvim_get_current_win()
+
+  return true
 end
 
-local function closed_infoview(failure_message, maintain, unopened)
-  local result
-  local this_infoview = infoview.get_current_infoview()
-
-  local buf = this_infoview.bufnr
-  local win = this_infoview.window
-
-  vim.list_extend(failure_message,
-  {
-    "Failed to close: ",
-    "maintain: " .. vim.inspect(maintain),
-    ("buf: %s, prev_buf: %s, buf valid: %s"):format(vim.inspect(buf), vim.inspect(prev_buf),
-      prev_buf and vim.inspect(vim.api.nvim_buf_is_valid(prev_buf))),
-    ("win: %s, prev_win: %s, win valid: %s"):format(vim.inspect(win), vim.inspect(prev_win),
-      prev_win and vim.inspect(vim.api.nvim_win_is_valid(prev_win))),
-    "is_open: " .. vim.inspect(this_infoview.is_open),
-    ("num_wins: %d, last_num_wins: %d"):format(helpers.get_num_wins(), last_num_wins)
-  })
-  if maintain then
-    result = not buf and not win and not prev_win and not prev_buf and not this_infoview.is_open
-      and helpers.get_num_wins() == last_num_wins
+local function created_win(_, arguments)
+  local new_wins = arguments[1]
+  if new_wins then
+    assert.update_wins(arguments[1], nil)
   else
-    vim.list_extend(failure_message, {"unopened: " .. vim.inspect(unopened)})
-    if unopened then
-      -- if not previously opened, we don't care about prev_win or prev_buf being accurate
-      result = not buf and not win and not this_infoview.is_open
-        and helpers.get_num_wins() == last_num_wins
-    else
-      -- make sure the previous window was closed
-      result = not this_infoview.is_open and not buf and not win and
-        prev_buf and not vim.api.nvim_buf_is_valid(prev_buf) and
-        prev_win and not vim.api.nvim_win_is_valid(prev_win) and
-        helpers.get_num_wins() == last_num_wins - 1
-    end
+    assert.changed_win()
+    assert.update_wins({vim.api.nvim_get_current_win()}, nil)
   end
 
-  prev_buf = buf
-  prev_win = win
+  return true
+end
 
-  return result
+local function closed_win(_, arguments)
+  local closed_wins = arguments[1]
+  if closed_wins then
+    assert.update_wins(nil, arguments[1])
+  else
+    -- inductive hypothesis: in addition to that of update_wins,
+    -- last_win must be the window we were in immediately before closing
+    assert.changed_win()
+    assert.update_wins(nil, {last_win})
+  end
+
+  return true
+end
+
+local function changed_win(_, _)
+  -- no nested assertion to allow for negation
+  return last_win ~= vim.api.nvim_get_current_win()
+end
+
+
+local function opened_infoview(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_truthy(this_info.is_open)
+  assert.is_truthy(this_info.bufnr)
+  assert.is_truthy(this_info.window)
+  assert.is_falsy(this_info.prev_buf)
+  assert.is_falsy(this_info.prev_win)
+
+  return true
+end
+
+local function opened_infoview_kept(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_truthy(this_info.is_open)
+  assert.is_truthy(this_info.bufnr)
+  assert.is_truthy(this_info.window)
+  assert.is_truthy(this_info.bufnr == this_info.prev_buf)
+  assert.is_truthy(this_info.window == this_info.prev_win)
+
+  return true
 end
 
-local function close_win()
-  local result = helpers.get_num_wins() == last_num_wins - 1
-  set_num_wins()
-  return result
+local function closed_infoview(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_falsy(this_info.is_open)
+  assert.is_falsy(this_info.bufnr)
+  assert.is_falsy(this_info.window)
+  assert.is_truthy(this_info.prev_buf)
+  assert.is_truthy(this_info.prev_win)
+
+  return true
 end
 
-local function new_win()
-  local result = helpers.get_num_wins() == last_num_wins + 1
-  set_num_wins()
-  return result
+local function closed_infoview_kept(_, arguments)
+  local this_info = arguments[1]
+
+  assert.is_falsy(this_info.is_open)
+  assert.is_falsy(this_info.bufnr)
+  assert.is_falsy(this_info.window)
+  assert.is_falsy(this_info.prev_buf)
+  assert.is_falsy(this_info.prev_win)
+
+  return true
 end
 
-local function infoview_check(state, checker, ...)
-  local failure_message = {}
+local function infoview_check(list)
+  local opened_wins = {}
+  local closed_wins = {}
+
+  for _, id in pairs(vim.api.nvim_list_tabpages()) do
+    local check = list[id]
+
+    local this_info = infoview._by_id[id]
+
+    -- infer check
+    if not check then
+      if this_info.prev_check == "opened" then
+        check = "opened_kept"
+      elseif this_info.prev_check == "opened_kept" then
+        check = "opened_kept"
+      elseif this_info.prev_check == "closed" then
+        check = "closed_kept"
+      elseif this_info.prev_check == "closed_kept" then
+        check = "closed_kept"
+      end
+    end
 
-  local result = checker(failure_message, ...)
+    if check == "opened" then
+      vim.list_extend(opened_wins, {this_info.window})
+      assert.opened_infoview_state(this_info)
+    elseif check == "opened_kept" then
+      assert.opened_infoview_kept_state(this_info)
+    elseif check == "closed" then
+      vim.list_extend(closed_wins, {this_info.prev_win})
+      assert.closed_infoview_state(this_info)
+    elseif check == "closed_kept" then
+      assert.closed_infoview_kept_state(this_info)
+    end
 
-  state.failure_message = table.concat(failure_message, "\n")
+    this_info.prev_buf = this_info.bufnr
+    this_info.prev_win = this_info.window
+    this_info.prev_check = check
+  end
 
-  set_num_wins()
+  assert.update_wins(opened_wins, closed_wins)
 
-  return result
+  return true
 end
 
 assert:register("assertion", "has_all", has_all)
-assert:register("assertion", "opened_infoview", function(state, _)
-  return infoview_check(state, opened_infoview, false)
+assert:register("assertion", "updated_infoviews", function(_, arguments)
+  return infoview_check(arguments[1] or {})
+end)
+assert:register("assertion", "opened_infoview", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "opened"})
 end)
-assert:register("assertion", "opened_infoview_kept", function(state, _)
-  return infoview_check(state, opened_infoview, true)
+assert:register("assertion", "opened_infoview_kept", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "opened_kept"})
 end)
-assert:register("assertion", "closed_infoview", function(state, _)
-  return infoview_check(state, closed_infoview, false, false)
+assert:register("assertion", "closed_infoview", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "closed"})
 end)
-assert:register("assertion", "closed_infoview_kept", function(state, _)
-  return infoview_check(state, closed_infoview, true, false)
+assert:register("assertion", "closed_infoview_kept", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "closed_kept"})
 end)
-assert:register("assertion", "unopened_infoview", function(state, _)
-  return infoview_check(state, closed_infoview, false, true)
+assert:register("assertion", "unopened_infoview", function(_, arguments)
+  return infoview_check(arguments[1] or {[vim.api.nvim_win_get_tabpage(0)] = "closed_kept"})
 end)
-assert:register("assertion", "change_infoview", change_infoview)
-assert:register("assertion", "close_win", close_win)
-assert:register("assertion", "new_win", new_win)
+
+-- internal state checks
+assert:register("assertion", "opened_infoview_state", opened_infoview)
+assert:register("assertion", "opened_infoview_kept_state", opened_infoview_kept)
+assert:register("assertion", "closed_infoview_state", closed_infoview)
+assert:register("assertion", "closed_infoview_kept_state", closed_infoview_kept)
+
+assert:register("assertion", "update_wins", update_wins)
+assert:register("assertion", "closed_win", closed_win)
+assert:register("assertion", "created_win", created_win)
+assert:register("assertion", "changed_win", changed_win)
+
+-- initialize on very first nvim window (base case satisfied pretty trivially)
+assert.created_win()
 
 return helpers
diff --git a/lua/tests/infoview/autoopen_spec.lua b/lua/tests/infoview/autoopen_spec.lua
index f16d0280..5948c289 100644
--- a/lua/tests/infoview/autoopen_spec.lua
+++ b/lua/tests/infoview/autoopen_spec.lua
@@ -15,7 +15,7 @@ describe('infoview', function()
   it('new tab automatically opens',
     function(_)
       vim.api.nvim_command('tabnew')
-      assert.new_win()
+      assert.created_win()
       vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
       assert.opened_infoview()
     end)
@@ -29,7 +29,7 @@ describe('infoview', function()
   it('opens automatically after having closen previous infoviews',
   function(_)
     vim.api.nvim_command("tabnew")
-    assert.new_win()
+    assert.created_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
     assert.opened_infoview()
   end)
@@ -38,7 +38,7 @@ describe('infoview', function()
   function(_)
     vim.api.nvim_command("tabnew")
     infoview.set_autoopen(false)
-    assert.new_win()
+    assert.created_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
     assert.unopened_infoview()
   end)
@@ -59,7 +59,7 @@ describe('infoview', function()
   function(_)
     vim.api.nvim_command("tabnew")
     infoview.set_autoopen(true)
-    assert.new_win()
+    assert.created_win()
     vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
     assert.opened_infoview()
   end)
diff --git a/lua/tests/infoview/close_all_spec.lua b/lua/tests/infoview/close_all_spec.lua
index 0a3737c7..b6724a00 100644
--- a/lua/tests/infoview/close_all_spec.lua
+++ b/lua/tests/infoview/close_all_spec.lua
@@ -4,51 +4,60 @@ require('tests.helpers').setup {
   infoview = {},
 }
 describe('infoview', function()
-  it('close_all succeeds',
-  function(_)
-    vim.api.nvim_command("edit temp.lean")
-    infoview.get_current_infoview():open()
-    assert.opened_infoview()
-
-    vim.api.nvim_command("tabnew")
-    assert.new_win()
-    vim.api.nvim_command("edit temp.lean")
-    infoview.get_current_infoview():open()
-    assert.opened_infoview()
-
-    vim.api.nvim_command("tabnew")
-    assert.new_win()
-    vim.api.nvim_command("edit temp.lean")
-    infoview.get_current_infoview():open()
-    assert.opened_infoview()
-    infoview.get_current_infoview():close()
-    assert.closed_infoview()
-
-    vim.api.nvim_command("tabnew")
-    assert.new_win()
-    vim.api.nvim_command("edit temp.lean")
-    infoview.get_current_infoview():open()
-    assert.opened_infoview()
-
-
-    local already_closed = false
-    local already_closed_count = 0
-    infoview.close_all(
-    function(info)
-      if info.window ~= vim.api.nvim_get_current_win() then
-        vim.api.nvim_set_current_win(info.window)
-        assert.change_infoview()
-      end
-      if not info.is_open then
-        already_closed = true
-        already_closed_count = already_closed_count + 1
-      end
-    end,
-    function()
-      assert.is_not.opened_infoview(already_closed)
-      already_closed = false
-    end
-    )
-    assert.equals(1, already_closed_count)
+  describe('close_all succeeds', function()
+    it('single infoview',
+    function(_)
+      local info_changes = {}
+
+      vim.api.nvim_command("edit temp.lean")
+      infoview.get_current_infoview():open()
+      assert.opened_infoview()
+      info_changes[vim.api.nvim_win_get_tabpage(0)] = "closed"
+
+      infoview.close_all()
+
+      assert.updated_infoviews(info_changes)
+    end)
+
+    it('multiple infoviews, not all opened',
+    function(_)
+      local info_changes = {}
+
+      vim.api.nvim_command("tabnew")
+      assert.created_win()
+      vim.api.nvim_command("edit temp.lean")
+      infoview.get_current_infoview():open()
+      assert.opened_infoview()
+      info_changes[vim.api.nvim_win_get_tabpage(0)] = "closed"
+
+      vim.api.nvim_command("tabnew")
+      assert.created_win()
+      vim.api.nvim_command("edit temp.lean")
+      infoview.get_current_infoview():open()
+      assert.opened_infoview()
+      info_changes[vim.api.nvim_win_get_tabpage(0)] = "closed"
+
+      vim.api.nvim_command("tabnew")
+      assert.created_win()
+      vim.api.nvim_command("edit temp.lean")
+      infoview.get_current_infoview():open()
+      assert.opened_infoview()
+      infoview.get_current_infoview():close()
+      assert.closed_infoview()
+      -- can actually omit this because it would be inferred by assert.updated_infoviews()
+      info_changes[vim.api.nvim_win_get_tabpage(0)] = "closed_kept"
+
+      vim.api.nvim_command("tabnew")
+      assert.created_win()
+      vim.api.nvim_command("edit temp.lean")
+      infoview.get_current_infoview():open()
+      assert.opened_infoview()
+      info_changes[vim.api.nvim_win_get_tabpage(0)] = "closed"
+
+
+      infoview.close_all()
+
+      assert.updated_infoviews(info_changes)
+    end)
   end)
 end)
diff --git a/lua/tests/infoview/run_spec.lua b/lua/tests/infoview/run_spec.lua
index 51edc653..d5e6dfb5 100644
--- a/lua/tests/infoview/run_spec.lua
+++ b/lua/tests/infoview/run_spec.lua
@@ -33,16 +33,18 @@ describe('infoview', function()
     it('remains closed on BufEnter',
     function(_)
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
+      -- would be equivalent to just do assert.updated_infoviews() here, because this would
+      -- correctly infer closed_infoview_kept; kept it (and others like it) for readability
       assert.closed_infoview_kept()
     end)
 
     it('remains closed on WinEnter',
     function(_)
       vim.api.nvim_command("split lua/tests/fixtures/example-lean3-project/test.lean")
-      assert.new_win()
+      assert.created_win()
       assert.closed_infoview_kept()
       vim.api.nvim_command("close")
-      assert.close_win()
+      assert.closed_win()
     end)
 
     it('CursorHold(I) disabled when closed',
@@ -90,14 +92,13 @@ describe('infoview', function()
       infoview.get_current_infoview():open()
       assert.opened_infoview()
       vim.api.nvim_command("tabnew")
-      assert.new_win()
+      assert.created_win()
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test.lean")
       assert.opened_infoview()
       infoview.get_current_infoview():close()
       assert.closed_infoview()
       assert.is_not.update_enabled()
       vim.api.nvim_command("tabprevious")
-      assert.change_infoview()
       assert.opened_infoview_kept()
     end)
 
@@ -116,7 +117,6 @@ describe('infoview', function()
     it('CursorHold(I) updated on WinEnter',
     function(_)
       vim.api.nvim_command("tabnext")
-      assert.change_infoview()
       assert.closed_infoview_kept()
       assert.is_not.update_enabled()
     end)
@@ -130,18 +130,14 @@ describe('infoview', function()
     it('opens independently',
     function(_)
       vim.api.nvim_command("tabprevious")
-      assert.change_infoview()
       infoview.get_current_infoview():close()
       assert.closed_infoview()
       vim.api.nvim_command("tabnext")
-      assert.change_infoview()
       infoview.get_current_infoview():open()
       assert.opened_infoview()
       vim.api.nvim_command("tabprevious")
-      assert.change_infoview()
       assert.closed_infoview_kept()
       vim.api.nvim_command("tabnext")
-      assert.change_infoview()
       assert.opened_infoview_kept()
     end)
 
diff --git a/lua/tests/infoview/start_spec.lua b/lua/tests/infoview/start_spec.lua
index 3443560d..3b55ffe3 100644
--- a/lua/tests/infoview/start_spec.lua
+++ b/lua/tests/infoview/start_spec.lua
@@ -29,7 +29,7 @@ describe('infoview', function()
     it('created valid distinct infoview',
       function(_)
         vim.api.nvim_command("tabnew")
-        assert.new_win()
+        assert.created_win()
         src_win = vim.api.nvim_get_current_win()
         vim.api.nvim_command('edit ' .. fixtures.lean_project.some_existing_file)
         assert.opened_infoview()

From 882a8751c0e9132f4ba2d873909983f520d83d3b Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Mon, 26 Jul 2021 07:32:12 -0700
Subject: [PATCH 09/13] Make `changed_win()` also set `last_win`.

---
 lua/tests/helpers.lua | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index 3ffff2cc..79fa73e7 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -183,7 +183,7 @@ local function created_win(_, arguments)
   if new_wins then
     assert.update_wins(arguments[1], nil)
   else
-    assert.changed_win()
+    assert.are_not.equal(last_win, vim.api.nvim_get_current_win())
     assert.update_wins({vim.api.nvim_get_current_win()}, nil)
   end
 
@@ -197,16 +197,19 @@ local function closed_win(_, arguments)
   else
     -- inductive hypothesis: in addition to that of update_wins,
     -- last_win must be the window we were in immediately before closing
-    assert.changed_win()
+    assert.are_not.equal(last_win, vim.api.nvim_get_current_win())
     assert.update_wins(nil, {last_win})
   end
 
   return true
 end
 
-local function changed_win(_, _)
+local function changed_win(state, _)
   -- no nested assertion to allow for negation
-  return last_win ~= vim.api.nvim_get_current_win()
+  local result = last_win ~= vim.api.nvim_get_current_win()
+  if state.mod and result then last_win = vim.api.nvim_get_current_win() end
+
+  return result
 end
 
 

From aa8b0db96b96b43c3fe1dae2169219f4d064384e Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Mon, 26 Jul 2021 11:11:56 -0700
Subject: [PATCH 10/13] Separate autocmd checking stuff from
 `infoview/run_spec.lua`.

---
 lua/tests/infoview/autocmd_spec.lua | 142 ++++++++++++++++++++++++++++
 lua/tests/infoview/run_spec.lua     | 128 +++++++------------------
 2 files changed, 175 insertions(+), 95 deletions(-)
 create mode 100644 lua/tests/infoview/autocmd_spec.lua

diff --git a/lua/tests/infoview/autocmd_spec.lua b/lua/tests/infoview/autocmd_spec.lua
new file mode 100644
index 00000000..fc5d1ad8
--- /dev/null
+++ b/lua/tests/infoview/autocmd_spec.lua
@@ -0,0 +1,142 @@
+local infoview = require('lean.infoview')
+local fixtures = require('tests.fixtures')
+
+require('tests.helpers').setup {}
+describe('infoview', function()
+  local function update_enabled(state, _)
+    local cursor_hold = string.find(vim.api.nvim_exec("autocmd CursorHold <buffer>", true), "LeanInfoviewUpdate")
+    local cursor_hold_i = string.find(vim.api.nvim_exec("autocmd CursorHoldI <buffer>", true), "LeanInfoviewUpdate")
+    if state.mod then
+      return cursor_hold and cursor_hold_i
+    end
+      return cursor_hold or cursor_hold_i
+  end
+
+  assert:register("assertion", "update_enabled", update_enabled)
+
+  describe('CursorHold(I)', function()
+    it('enabled when opened',
+    function(_)
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+      infoview.get_current_infoview():open()
+      assert.opened_infoview()
+      assert.update_enabled()
+    end)
+
+    it('remains enabled on BufEnter',
+    function(_)
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_nested_existing_file)
+      assert.opened_infoview_kept()
+      assert.update_enabled()
+    end)
+
+    it('remains enabled on WinEnter',
+    function(_)
+      vim.api.nvim_command('split ' .. fixtures.lean3_project.some_existing_file)
+      assert.created_win()
+      assert.opened_infoview_kept()
+      assert.update_enabled()
+
+      vim.api.nvim_command("close")
+      assert.closed_win()
+
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+      assert.opened_infoview_kept()
+    end)
+
+    it('disabled when closed',
+    function(_)
+      infoview.get_current_infoview():close()
+      assert.closed_infoview()
+      assert.is_not.update_enabled()
+    end)
+
+    it('remains disabled on BufEnter',
+    function(_)
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_nested_existing_file)
+      assert.closed_infoview_kept()
+      assert.is_not.update_enabled()
+    end)
+
+    it('remains disabled on WinEnter',
+    function(_)
+      vim.api.nvim_command('split ' .. fixtures.lean3_project.some_existing_file)
+      assert.created_win()
+      assert.closed_infoview_kept()
+      assert.is_not.update_enabled()
+
+      vim.api.nvim_command("close")
+      assert.closed_win()
+
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+      assert.closed_infoview_kept()
+    end)
+
+    it('re-enabled when re-opened',
+    function(_)
+      infoview.get_current_infoview():open()
+      assert.opened_infoview()
+      assert.update_enabled()
+    end)
+    describe('new tab', function()
+      it('disables independently',
+      function(_)
+        vim.api.nvim_command("tabnew")
+        assert.created_win()
+        vim.api.nvim_command("edit " .. fixtures.lean_project.some_existing_file)
+        assert.unopened_infoview()
+        assert.is_not.update_enabled()
+        vim.api.nvim_command("tabprevious")
+        assert.changed_win()
+        assert.opened_infoview_kept()
+        assert.update_enabled()
+      end)
+
+      it('enables independently',
+      function(_)
+        infoview.get_current_infoview():close()
+        assert.closed_infoview()
+        assert.is_not.update_enabled()
+        vim.api.nvim_command("tabnext")
+        assert.changed_win()
+        infoview.get_current_infoview():open()
+        assert.opened_infoview()
+        assert.update_enabled()
+        vim.api.nvim_command("tabprevious")
+        assert.changed_win()
+        assert.closed_infoview_kept()
+        assert.is_not.update_enabled()
+      end)
+
+      it('does not enable on irrelevant file BufEnter',
+      function(_)
+        vim.api.nvim_command("tabnext")
+        assert.changed_win()
+        assert.opened_infoview_kept()
+        assert.update_enabled()
+        vim.api.nvim_command("edit temp")
+        assert.opened_infoview_kept()
+        assert.is_not.update_enabled()
+      end)
+
+      it('does not enable when re-opening on irrelevant file',
+      function(_)
+        infoview.get_current_infoview():close()
+        assert.closed_infoview()
+        assert.is_not.update_enabled()
+        infoview.get_current_infoview():open()
+        assert.opened_infoview()
+        assert.is_not.update_enabled()
+      end)
+
+      it('enabled on relevant file BufEnter',
+      function(_)
+        vim.api.nvim_command("edit " .. fixtures.lean_project.some_existing_file)
+        assert.opened_infoview_kept()
+        assert.update_enabled()
+      end)
+    end)
+  end)
+
+
+end)
diff --git a/lua/tests/infoview/run_spec.lua b/lua/tests/infoview/run_spec.lua
index d5e6dfb5..a5df69ec 100644
--- a/lua/tests/infoview/run_spec.lua
+++ b/lua/tests/infoview/run_spec.lua
@@ -1,38 +1,43 @@
 local infoview = require('lean.infoview')
 local fixtures = require('tests.fixtures')
 
-require('tests.helpers').setup {
-  infoview = { autoopen = true },
-}
+require('tests.helpers').setup{}
 describe('infoview', function()
-  local function update_enabled(state, _)
-    local cursor_hold = string.find(vim.api.nvim_exec("autocmd CursorHold <buffer>", true), "LeanInfoviewUpdate")
-    local cursor_hold_i = string.find(vim.api.nvim_exec("autocmd CursorHoldI <buffer>", true), "LeanInfoviewUpdate")
-    if state.mod then
-      return cursor_hold and cursor_hold_i
-    end
-      return cursor_hold or cursor_hold_i
-  end
-
-  assert:register("assertion", "update_enabled", update_enabled)
-
   describe('initial', function()
-    it('CursorHold(I) enabled when opened',
+    it('opens',
     function(_)
-      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+      vim.api.nvim_command("edit " .. fixtures.lean3_project.some_existing_file)
+      infoview.get_current_infoview():open()
       assert.opened_infoview()
-      assert.update_enabled()
+    end)
+
+    it('remains open on BufEnter',
+    function(_)
+      vim.api.nvim_command("edit " .. fixtures.lean3_project.some_existing_file)
+      assert.opened_infoview_kept()
+    end)
+
+    it('remains open on WinEnter',
+    function(_)
+      vim.api.nvim_command("split " .. fixtures.lean3_project.some_existing_file)
+      assert.created_win()
+      assert.opened_infoview_kept()
+      vim.api.nvim_command("close")
+      assert.closed_win()
+      assert.opened_infoview_kept()
     end)
 
     it('closes',
     function(_)
+      vim.api.nvim_command('edit ' .. fixtures.lean3_project.some_existing_file)
+      assert.opened_infoview_kept()
       infoview.get_current_infoview():close()
       assert.closed_infoview()
     end)
 
     it('remains closed on BufEnter',
     function(_)
-      vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test/test1.lean")
+      vim.api.nvim_command("edit " .. fixtures.lean3_project.some_nested_existing_file)
       -- would be equivalent to just do assert.updated_infoviews() here, because this would
       -- correctly infer closed_infoview_kept; kept it (and others like it) for readability
       assert.closed_infoview_kept()
@@ -40,38 +45,20 @@ describe('infoview', function()
 
     it('remains closed on WinEnter',
     function(_)
-      vim.api.nvim_command("split lua/tests/fixtures/example-lean3-project/test.lean")
+      vim.api.nvim_command("split " .. fixtures.lean3_project.some_existing_file)
       assert.created_win()
       assert.closed_infoview_kept()
       vim.api.nvim_command("close")
       assert.closed_win()
+      assert.closed_infoview_kept()
     end)
 
-    it('CursorHold(I) disabled when closed',
-    function(_)
-      assert.is_not.update_enabled()
-    end)
-
-    it('opens',
+    it('manual quit succeeds and updates internal state',
     function(_)
       infoview.get_current_infoview():open()
       assert.opened_infoview()
-    end)
-
-    it('remains open on BufWinEnter',
-    function(_)
-      vim.api.nvim_command("edit lua/tests/fixtures/example-lean3-project/test.lean")
-      assert.opened_infoview_kept()
-    end)
-
-    it('CursorHold(I) enabled when re-opened',
-    function(_)
-      assert.update_enabled()
-    end)
-
-    it('manual quit succeeds and updates internal state',
-    function(_)
       vim.api.nvim_command("wincmd l")
+      assert.changed_win()
       vim.api.nvim_command("quit")
       assert.closed_infoview()
     end)
@@ -81,6 +68,7 @@ describe('infoview', function()
       infoview.get_current_infoview():open()
       assert.opened_infoview()
       vim.api.nvim_command("wincmd l")
+      assert.changed_win()
       vim.api.nvim_command("close")
       assert.closed_infoview()
     end)
@@ -94,79 +82,29 @@ describe('infoview', function()
       vim.api.nvim_command("tabnew")
       assert.created_win()
       vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test.lean")
+      infoview.get_current_infoview():open()
       assert.opened_infoview()
       infoview.get_current_infoview():close()
       assert.closed_infoview()
-      assert.is_not.update_enabled()
       vim.api.nvim_command("tabprevious")
+      assert.changed_win()
       assert.opened_infoview_kept()
     end)
 
-    it('CursorHold(I) disabled independently',
-    function(_)
-      assert.is.update_enabled()
-    end)
-
-    it('CursorHold(I) updated on BufEnter',
-    function(_)
-      vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test.lean")
-      assert.opened_infoview_kept()
-      assert.is.update_enabled()
-    end)
-
-    it('CursorHold(I) updated on WinEnter',
-    function(_)
-      vim.api.nvim_command("tabnext")
-      assert.closed_infoview_kept()
-      assert.is_not.update_enabled()
-    end)
-
-    it('remains closed on BufWinEnter',
-    function(_)
-      vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
-      assert.closed_infoview_kept()
-    end)
-
     it('opens independently',
     function(_)
-      vim.api.nvim_command("tabprevious")
       infoview.get_current_infoview():close()
       assert.closed_infoview()
       vim.api.nvim_command("tabnext")
+      assert.changed_win()
       infoview.get_current_infoview():open()
       assert.opened_infoview()
       vim.api.nvim_command("tabprevious")
+      assert.changed_win()
       assert.closed_infoview_kept()
       vim.api.nvim_command("tabnext")
+      assert.changed_win()
       assert.opened_infoview_kept()
     end)
-
-    it('remains open on BufWinEnter',
-    function(_)
-      vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
-      assert.opened_infoview_kept()
-    end)
-
-    it('does not set CursorHold(I) on irrelevant file BufEnter',
-    function(_)
-      vim.api.nvim_command("edit temp")
-      assert.opened_infoview_kept()
-      assert.is_not.update_enabled()
-    end)
-
-    it('does not set CursorHold(I) when re-opening on irrelevant file',
-    function(_)
-      infoview.get_current_infoview():close()
-      assert.closed_infoview()
-      infoview.get_current_infoview():open()
-      assert.opened_infoview()
-      assert.is_not.update_enabled()
-    end)
-
-    it('updates CursorHold(I) on relevant file BufEnter',
-    function(_)
-      vim.api.nvim_command("edit lua/tests/fixtures/example-lean4-project/Test/Test1.lean")
-      assert.update_enabled()
-    end)
   end)
 end)

From 1ae1809fe02bb14c3590d140b9fdc007414e3baf Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Mon, 26 Jul 2021 11:21:09 -0700
Subject: [PATCH 11/13] Iterate infoviews by id rather than by tabpage.

---
 lua/tests/helpers.lua | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index 79fa73e7..93fe19ae 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -265,13 +265,13 @@ local function infoview_check(list)
   local opened_wins = {}
   local closed_wins = {}
 
-  for _, id in pairs(vim.api.nvim_list_tabpages()) do
+  for id, this_info in pairs(infoview._by_id) do
     local check = list[id]
 
-    local this_info = infoview._by_id[id]
-
-    -- infer check
     if not check then
+      -- all unspecified infoviews must have previously been accounted for
+      assert.is_truthy(this_info.prev_check)
+      -- infer check
       if this_info.prev_check == "opened" then
         check = "opened_kept"
       elseif this_info.prev_check == "opened_kept" then

From 9c6eac80bbdbe9685211bbe417036af06ade3723 Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Mon, 26 Jul 2021 11:40:59 -0700
Subject: [PATCH 12/13] Make separate `kept_win` assertion to allow
 `update_wins` assertion within `changed_win`.

---
 lua/tests/helpers.lua | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index 93fe19ae..3d078f59 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -204,14 +204,19 @@ local function closed_win(_, arguments)
   return true
 end
 
-local function changed_win(state, _)
-  -- no nested assertion to allow for negation
-  local result = last_win ~= vim.api.nvim_get_current_win()
-  if state.mod and result then last_win = vim.api.nvim_get_current_win() end
+local function changed_win(_, _)
+  assert.are_not.equal(last_win, vim.api.nvim_get_current_win())
 
-  return result
+  assert.update_wins()
+  return true
 end
 
+local function kept_win(_, _)
+  assert.are_equal(last_win, vim.api.nvim_get_current_win())
+
+  assert.update_wins()
+  return true
+end
 
 local function opened_infoview(_, arguments)
   local this_info = arguments[1]
@@ -335,6 +340,7 @@ assert:register("assertion", "update_wins", update_wins)
 assert:register("assertion", "closed_win", closed_win)
 assert:register("assertion", "created_win", created_win)
 assert:register("assertion", "changed_win", changed_win)
+assert:register("assertion", "kept_win", kept_win)
 
 -- initialize on very first nvim window (base case satisfied pretty trivially)
 assert.created_win()

From 05fcb4dd3ed468c514ae50dca958493b869f0b9f Mon Sep 17 00:00:00 2001
From: Rishikesh Vaishnav <rishhvaishnav@gmail.com>
Date: Mon, 26 Jul 2021 11:53:55 -0700
Subject: [PATCH 13/13] Make sure all specified infoviews were actually checked
 in `infoview_check`.

---
 lua/tests/helpers.lua | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua
index 3d078f59..b3c49710 100644
--- a/lua/tests/helpers.lua
+++ b/lua/tests/helpers.lua
@@ -286,6 +286,8 @@ local function infoview_check(list)
       elseif this_info.prev_check == "closed_kept" then
         check = "closed_kept"
       end
+    else
+      this_info.checked = true
     end
 
     if check == "opened" then
@@ -305,6 +307,13 @@ local function infoview_check(list)
     this_info.prev_check = check
   end
 
+  -- make sure all specified infoviews were hit
+  for id, check in pairs(list) do
+    assert.is_truthy(infoview._by_id[id].checked)
+    assert.are_equal(check, infoview._by_id[id].prev_check)
+    infoview._by_id[id].checked = nil
+  end
+
   assert.update_wins(opened_wins, closed_wins)
 
   return true