Split the clean_buffer helper for lean3, simplifying it.

.luacheckrc

@@ -1,5 +1,4 @@
 globals = {
-  "_clean_buffer_count",
   "vim",
   "lean_nvim_default_filetype",
   "describe",

lua/tests/abbreviations/abbreviations_spec.lua

@@ -12,44 +12,44 @@ end
 require('lean').setup {}
 
 describe('unicode abbreviation expansion', function()
-  it('autoexpands abbreviations', helpers.clean_buffer('lean', '', function()
+  it('autoexpands abbreviations', helpers.clean_buffer(function()
     helpers.insert[[\a]]
     assert.contents.are[[α]]
   end))
 
   describe('explicit triggers', function()
-    it('inserts a space on <Space>', helpers.clean_buffer('lean', '', function()
+    it('inserts a space on <Space>', helpers.clean_buffer(function()
       helpers.insert[[\e<Space>]]
       wait_for_expansion()
       assert.contents.are[[ε ]]
     end))
 
-    it('inserts a newline on <CR>', helpers.clean_buffer('lean', '', function()
+    it('inserts a newline on <CR>', helpers.clean_buffer(function()
       helpers.insert[[\e<CR>]]
       wait_for_expansion()
       assert.contents.are('ε\n')
     end))
 
-    it('inserts nothing on <Tab>', helpers.clean_buffer('lean', '', function()
+    it('inserts nothing on <Tab>', helpers.clean_buffer(function()
       helpers.insert[[\e<Tab>]]
       wait_for_expansion()
       assert.contents.are[[ε]]
     end))
 
-    it('leaves the cursor in the right spot on <Tab>', helpers.clean_buffer('lean', '', function()
+    it('leaves the cursor in the right spot on <Tab>', helpers.clean_buffer(function()
       helpers.insert[[\<<Tab>abc]]
       wait_for_expansion()
       assert.contents.are[[⟨abc]]
     end))
 
-    it('inserts nothing on <Tab> mid-line', helpers.clean_buffer('lean', 'foo bar baz quux,', function()
+    it('inserts nothing on <Tab> mid-line', helpers.clean_buffer('foo bar baz quux,', function()
       vim.cmd.normal('$')
       helpers.insert[[ \comp<Tab> spam]]
       wait_for_expansion()
       assert.contents.are[[foo bar baz quux ∘ spam,]]
     end))
 
-    it('does not interfere with existing mappings', helpers.clean_buffer('lean', '', function()
+    it('does not interfere with existing mappings', helpers.clean_buffer(function()
       vim.api.nvim_buf_set_keymap(
           0,
           'i',
@@ -68,7 +68,7 @@ describe('unicode abbreviation expansion', function()
       vim.api.nvim_buf_del_keymap(0, 'i', '<Tab>')
     end))
 
-    it('does not interfere with existing lua mappings', helpers.clean_buffer('lean', '', function()
+    it('does not interfere with existing lua mappings', helpers.clean_buffer(function()
       vim.b.foo = 0
       local inc = function() vim.b.foo = vim.b.foo + 1 end
 
@@ -92,17 +92,17 @@ describe('unicode abbreviation expansion', function()
   end)
 
   -- Really this needs to place the cursor too, but for now we just strip
-  it('handles placing the $CURSOR', helpers.clean_buffer('lean', '', function()
+  it('handles placing the $CURSOR', helpers.clean_buffer(function()
     helpers.insert[[foo \<><Tab>bar, baz]]
     assert.current_line.is('foo ⟨bar, baz⟩')
   end))
 
-  it('expands mid-word', helpers.clean_buffer('lean', '', function()
+  it('expands mid-word', helpers.clean_buffer(function()
     helpers.insert[[(\a]]
     assert.contents.are[[(α]]
   end))
 
-  it('expands abbreviations in command mode', helpers.clean_buffer('lean', '', function()
+  it('expands abbreviations in command mode', helpers.clean_buffer(function()
     helpers.insert[[foo ε bar]]
     vim.cmd.normal('$')
     helpers.feed[[q/a\e<Space><CR>ibaz]]

lua/tests/diagnostics_spec.lua

@@ -4,9 +4,7 @@ local lean_lsp_diagnostics = require('lean._util').lean_lsp_diagnostics
 require('lean').setup { lsp = { enable = true } }
 
 describe('diagnostics', function()
-  it('are retrieved from the server', helpers.clean_buffer('lean',
-    [[ example : False := by trivial ]],
-  function()
+  it('are retrieved from the server', helpers.clean_buffer([[ example : False := by trivial ]], function()
     helpers.wait_for_line_diagnostics()
     local diags = lean_lsp_diagnostics()
     assert.are_equal(1, #diags)

lua/tests/helpers.lua

@@ -119,29 +119,32 @@ end
 
 -- Even though we can delete a buffer, so should be able to reuse names,
 -- we do this to ensure if a test fails, future ones still get new "files".
-local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr, ft)
+local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr)
   local counter = helpers._clean_buffer_counter
   helpers._clean_buffer_counter = helpers._clean_buffer_counter + 1
-  local unique_name =
-    ft == 'lean3' and string.format('unittest-%d.lean', counter)
-                   or string.format('%s/unittest-%d.lean', fixtures.lean_project.path, counter)
+  local unique_name = string.format('%s/unittest-%d.lean', fixtures.lean_project.path, counter)
   vim.api.nvim_buf_set_name(bufnr, unique_name)
 end
 
---- Create a clean Lean buffer of the given filetype with the given contents.
+--- Create a clean Lean buffer with the given contents.
 --
 --  Waits for the LSP to be ready before proceeding with a given callback.
 --
 --  Yes c(lean) may be a double entendre, and no I don't feel bad.
-function helpers.clean_buffer(ft, contents, callback)
+function helpers.clean_buffer(contents, callback)
+  if callback == nil then
+    callback = contents
+    contents = ''
+  end
+
   return function()
     local bufnr = vim.api.nvim_create_buf(false, false)
-    set_unique_name_so_we_always_have_a_separate_fake_file(bufnr, ft)
+    set_unique_name_so_we_always_have_a_separate_fake_file(bufnr)
     -- apparently necessary to trigger BufWinEnter
     vim.api.nvim_set_current_buf(bufnr)
     vim.opt_local.bufhidden = "hide"
     vim.opt_local.swapfile = false
-    vim.opt.filetype = ft
+    vim.opt.filetype = 'lean'
 
     vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, vim.split(contents, '\n'))
     vim.api.nvim_buf_call(bufnr, function() callback{ source_file = { bufnr = bufnr } } end)

lua/tests/infoview/contents_spec.lua

@@ -281,7 +281,7 @@ describe('infoview content (auto-)update', function()
     end)
   end)
 
-  describe('cursor position', helpers.clean_buffer('lean', '', function()
+  describe('cursor position', helpers.clean_buffer(function()
     it('is set to the goal line', function()
       local lines = { 'example ' }
       for i=1, 100 do
@@ -301,7 +301,7 @@ describe('infoview content (auto-)update', function()
     end)
   end))
 
-  describe('processing message', helpers.clean_buffer('lean', '#eval IO.sleep 5000', function()
+  describe('processing message', helpers.clean_buffer('#eval IO.sleep 5000', function()
     it('is shown while a file is processing', function()
       local uri = vim.uri_from_fname(vim.api.nvim_buf_get_name(0))
       local result = vim.wait(15000, function() return require('lean.progress').is_processing(uri) end)

lua/tests/infoview/pin_spec.lua

@@ -7,7 +7,7 @@ local helpers = require('tests.helpers')
 
 require('lean').setup{ lsp = { enable = true } }
 
-describe('infoview pins', helpers.clean_buffer('lean', dedent[[
+describe('infoview pins', helpers.clean_buffer(dedent[[
   theorem has_tactic_goal : p ∨ q → q ∨ p := by
     intro h
     cases h with

lua/tests/infoview/widgets_spec.lua

@@ -7,7 +7,7 @@ local helpers = require('tests.helpers')
 
 require('lean').setup{}
 
-describe('infoview widgets', helpers.clean_buffer('lean', '#check Nat', function()
+describe('infoview widgets', helpers.clean_buffer('#check Nat', function()
 
   local lean_window = vim.api.nvim_get_current_win()
   local current_infoview = infoview.get_current_infoview()

lua/tests/language_support_spec.lua

@@ -8,12 +8,12 @@ local helpers = require('tests.helpers')
 require('lean').setup{}
 
 describe('commenting', function()
-  it('comments out single lines', helpers.clean_buffer('lean', 'def best := 37', function()
+  it('comments out single lines', helpers.clean_buffer('def best := 37', function()
     vim.cmd.TComment()
     assert.contents.are('-- def best := 37')
   end))
 
-  it('comments out multiple lines inline by default', helpers.clean_buffer('lean', [[
+  it('comments out multiple lines inline by default', helpers.clean_buffer([[
 def foo := 12
 def bar := 37]], function()
     vim.cmd(':% TComment')
@@ -23,7 +23,7 @@ def bar := 37]], function()
     ]])
   end))
 
-  it('can comment out block comments', helpers.clean_buffer('lean', [[
+  it('can comment out block comments', helpers.clean_buffer([[
 def foo := 12
 def bar := 37]], function()
     vim.cmd(':% TCommentBlock')

lua/tests/lean3/abbreviations_spec.lua

@@ -1,4 +1,5 @@
 local helpers = require('tests.helpers')
+local clean_buffer = require('tests.lean3.helpers').clean_buffer
 
 -- Wait some time for the abbreviation to have been expanded.
 -- This is very naive, it just ensures the line contains no `\`.
@@ -12,44 +13,44 @@ end
 require('lean').setup {}
 
 helpers.if_has_lean3('unicode abbreviation expansion', function()
-  it('autoexpands abbreviations', helpers.clean_buffer('lean3', '', function()
+  it('autoexpands abbreviations', clean_buffer(function()
     helpers.insert[[\a]]
     assert.contents.are[[α]]
   end))
 
   describe('explicit triggers', function()
-    it('inserts a space on <Space>', helpers.clean_buffer('lean3', '', function()
+    it('inserts a space on <Space>', clean_buffer(function()
       helpers.insert[[\e<Space>]]
       wait_for_expansion()
       assert.contents.are[[ε ]]
     end))
 
-    it('inserts a newline on <CR>', helpers.clean_buffer('lean3', '', function()
+    it('inserts a newline on <CR>', clean_buffer(function()
       helpers.insert[[\e<CR>]]
       wait_for_expansion()
       assert.contents.are('ε\n')
     end))
 
-    it('inserts nothing on <Tab>', helpers.clean_buffer('lean3', '', function()
+    it('inserts nothing on <Tab>', clean_buffer(function()
       helpers.insert[[\e<Tab>]]
       wait_for_expansion()
       assert.contents.are[[ε]]
     end))
 
-    it('leaves the cursor in the right spot on <Tab>', helpers.clean_buffer('lean3', '', function()
+    it('leaves the cursor in the right spot on <Tab>', clean_buffer(function()
       helpers.insert[[\<<Tab>abc]]
       wait_for_expansion()
       assert.contents.are[[⟨abc]]
     end))
 
-    it('inserts nothing on <Tab> mid-line', helpers.clean_buffer('lean3', 'foo bar baz quux,', function()
+    it('inserts nothing on <Tab> mid-line', clean_buffer('foo bar baz quux,', function()
       vim.cmd.normal('$')
       helpers.insert[[ \comp<Tab> spam]]
       wait_for_expansion()
       assert.contents.are[[foo bar baz quux ∘ spam,]]
     end))
 
-    it('does not interfere with existing mappings', helpers.clean_buffer('lean3', '', function()
+    it('does not interfere with existing mappings', clean_buffer(function()
       vim.api.nvim_buf_set_keymap(
           0,
           'i',
@@ -68,7 +69,7 @@ helpers.if_has_lean3('unicode abbreviation expansion', function()
       vim.api.nvim_buf_del_keymap(0, 'i', '<Tab>')
     end))
 
-    it('does not interfere with existing lua mappings', helpers.clean_buffer('lean3', '', function()
+    it('does not interfere with existing lua mappings', clean_buffer(function()
       vim.b.foo = 0
       local inc = function() vim.b.foo = vim.b.foo + 1 end
 
@@ -92,17 +93,17 @@ helpers.if_has_lean3('unicode abbreviation expansion', function()
   end)
 
   -- Really this needs to place the cursor too, but for now we just strip
-  it('handles placing the $CURSOR', helpers.clean_buffer('lean3', '', function()
+  it('handles placing the $CURSOR', clean_buffer(function()
     helpers.insert[[foo \<><Tab>bar, baz]]
     assert.current_line.is('foo ⟨bar, baz⟩')
   end))
 
-  it('expands mid-word', helpers.clean_buffer('lean3', '', function()
+  it('expands mid-word', clean_buffer(function()
     helpers.insert[[(\a]]
     assert.contents.are[[(α]]
   end))
 
-  it('expands abbreviations in command mode', helpers.clean_buffer('lean3', '', function()
+  it('expands abbreviations in command mode', clean_buffer(function()
     helpers.insert[[foo ε bar]]
     vim.cmd.normal('$')
     helpers.feed[[q/a\e<Space><CR>ibaz]]

lua/tests/lean3/diagnostics_spec.lua

@@ -1,11 +1,11 @@
+local clean_buffer = require('tests.lean3.helpers').clean_buffer
 local helpers = require('tests.helpers')
 local lean_lsp_diagnostics = require('lean._util').lean_lsp_diagnostics
 
 require('lean').setup { lsp3 = { enable = true } }
 
 helpers.if_has_lean3('diagnostics', function()
-  it('are retrieved from the server', helpers.clean_buffer('lean3',
-    [[ example : false := by trivial ]],
+  it('are retrieved from the server', clean_buffer([[ example : false := by trivial ]],
   function()
     helpers.wait_for_line_diagnostics()
     local diags = lean_lsp_diagnostics()

lua/tests/lean3/helpers.lua

@@ -0,0 +1,37 @@
+local helpers = { _clean_buffer_counter = 1 }
+
+-- Even though we can delete a buffer, so should be able to reuse names,
+-- we do this to ensure if a test fails, future ones still get new "files".
+local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr)
+  local counter = helpers._clean_buffer_counter
+  helpers._clean_buffer_counter = helpers._clean_buffer_counter + 1
+  local unique_name = string.format('unittest-%d.lean', counter)
+  vim.api.nvim_buf_set_name(bufnr, unique_name)
+end
+
+--- Create a clean Lean buffer with the given contents.
+--
+--  Waits for the LSP to be ready before proceeding with a given callback.
+--
+--  Yes c(lean) may be a double entendre, and no I don't feel bad.
+function helpers.clean_buffer(contents, callback)
+  if callback == nil then
+    callback = contents
+    contents = ''
+  end
+
+  return function()
+    local bufnr = vim.api.nvim_create_buf(false, false)
+    set_unique_name_so_we_always_have_a_separate_fake_file(bufnr)
+    -- apparently necessary to trigger BufWinEnter
+    vim.api.nvim_set_current_buf(bufnr)
+    vim.opt_local.bufhidden = 'hide'
+    vim.opt_local.swapfile = false
+    vim.opt.filetype = 'lean3'
+
+    vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, vim.split(contents, '\n'))
+    vim.api.nvim_buf_call(bufnr, function() callback{ source_file = { bufnr = bufnr } } end)
+  end
+end
+
+return helpers

lua/tests/lean3/infoview/contents_spec.lua

@@ -1,3 +1,4 @@
+local clean_buffer = require('tests.lean3.helpers').clean_buffer
 local infoview = require('lean.infoview')
 local fixtures = require('tests.fixtures')
 local helpers = require('tests.helpers')
@@ -63,7 +64,7 @@ helpers.if_has_lean3('components', function()
     end)
   end
 
-  describe('cursor position', helpers.clean_buffer('lean3', '', function()
+  describe('cursor position', clean_buffer(function()
     it('is set to the goal line', function()
       local lines = { 'example ' }
       for i=1, 100 do

lua/tests/lean3/infoview/widgets_spec.lua

@@ -1,9 +1,10 @@
+local clean_buffer = require('tests.lean3.helpers').clean_buffer
 local helpers = require('tests.helpers')
 local infoview = require('lean.infoview')
 
 require('lean').setup {}
 
-helpers.if_has_lean3('infoview widgets', helpers.clean_buffer('lean3', 'example : 2 = 2 := by refl', function()
+helpers.if_has_lean3('infoview widgets', clean_buffer('example : 2 = 2 := by refl', function()
 
   local lean_window = vim.api.nvim_get_current_win()
   local current_infoview = infoview.get_current_infoview()

lua/tests/lean3/language_support_spec.lua

@@ -2,18 +2,19 @@
 --- Tests for basic Lean language support.
 ---@brief ]]
 
+local clean_buffer = require('tests.lean3.helpers').clean_buffer
 local dedent = require('lean._util').dedent
 local helpers = require('tests.helpers')
 
 require('lean').setup{}
 
 helpers.if_has_lean3('commenting', function()
-  it('comments out single lines', helpers.clean_buffer('lean3', 'def best := 37', function()
+  it('comments out single lines', clean_buffer('def best := 37', function()
     vim.cmd.TComment()
     assert.contents.are('-- def best := 37')
   end))
 
-  it('comments out multiple lines inline by default', helpers.clean_buffer('lean3', [[
+  it('comments out multiple lines inline by default', clean_buffer([[
 def foo := 12
 def bar := 37]], function()
     vim.cmd(':% TComment')
@@ -23,7 +24,7 @@ def bar := 37]], function()
     ]])
   end))
 
-  it('can comment out block comments', helpers.clean_buffer('lean3', [[
+  it('can comment out block comments', clean_buffer([[
 def foo := 12
 def bar := 37]], function()
     vim.cmd(':% TCommentBlock')