Fix the infoview containing a trailing newline in one case.

It was when interactive diagnostics are present.

This is the main functional change of this commit -- but as part of it,
the behavior of dedent as well as assert.contents and friends from the
testing helpers have all changed to be what (to me) is more logical.

This is the case even though there's still one "magic" behavior (in
a new helper function _expected) which seems required to get a test in
the abbreviations spec to pass.

Also added here therefore are a bunch of tests for the testing helpers
(and for dedent) which all pass and should help ensure that all this
delicate code continues to work if it needs tweaking again.

A secondary tweak to the testing helpers is that assert.contents and
friends now automatically dedent their expected value, which makes the
tests a bit more prettily indented.

All the tests are then also refactored to use that "uniform" style for
asserting against their contents, which is most of the whitespace change
noise.

lua/lean/_util.lua

@@ -102,9 +102,9 @@ end
 ---
 --- REPLACEME: plenary.nvim has a version of this but it has odd behavior.
 function M.dedent(str)
-  str = str:gsub(" +$", ""):gsub("^ +", "") -- remove spaces at start and end
+  str = str:gsub('^ +', ''):gsub('\n *$', '\n') -- trim leading/trailing space
   local prefix = max_common_indent(str)
-  return (str:gsub("\n" .. prefix, "\n"):gsub("\n$", ""))
+  return str:gsub('\n' .. prefix, '\n')
 end
 
 function M.load_mappings(mappings, buffer)

lua/lean/infoview/components.lua

@@ -70,7 +70,7 @@ function components.term_goal(term_goal)
 
   return {
     Element:new{
-      text = H(string.format('expected type (%s)', range_to_string(term_goal.range)) .. "\n" .. term_goal.goal),
+      text = H(('expected type (%s)'):format(range_to_string(term_goal.range)) .. '\n' .. term_goal.goal),
       name = 'term-goal'
     }
   }
@@ -308,7 +308,7 @@ local function tagged_text_msg_embed(t, sess, parent_cls)
   local element = Element:new{ name = 'code-with-infos' }
 
   if t.text ~= nil then
-    element.text = t.text
+    element.text = t.text:gsub('\n$', '')
   elseif t.append ~= nil then
     for _, s in ipairs(t.append) do
       element:add_child(tagged_text_msg_embed(s, sess))
@@ -441,9 +441,9 @@ function components.interactive_diagnostics(diags, line, sess)
           text = H(string.format('%s: %s:\n',
             range_to_string(diag.range),
             util.DIAGNOSTIC_SEVERITY[diag.severity])),
-          name = 'diagnostic'
+          name = 'diagnostic',
+          children = { tagged_text_msg_embed(diag.message, sess) }
       }
-      element:add_child(tagged_text_msg_embed(diag.message, sess))
       table.insert(elements, element)
     end
   end

lua/tests/helpers.lua

@@ -140,9 +140,14 @@ end
 --
 --  Yes c(lean) may be a double entendre, and no I don't feel bad.
 function helpers.clean_buffer(contents, callback)
+  local lines
+
+  -- Support a 1-arg version where we assume the contents is an empty buffer.
   if callback == nil then
     callback = contents
-    contents = ''
+    lines = {}
+  else
+    lines = vim.split(util.dedent(contents:gsub('^\n', '')):gsub('\n$', ''), '\n')
   end
 
   return function()
@@ -154,7 +159,7 @@ function helpers.clean_buffer(contents, callback)
     vim.opt_local.swapfile = false
     vim.opt.filetype = 'lean'
 
-    vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, vim.split(contents, '\n'))
+    vim.api.nvim_buf_set_lines(bufnr, 0, -1, false, lines)
     vim.api.nvim_buf_call(bufnr, function() callback{ source_file = { bufnr = bufnr } } end)
   end
 end
@@ -206,29 +211,37 @@ local function has_current_window(_, arguments)
 end
 assert:register('assertion', 'current_window', has_current_window)
 
+local function _expected(arguments)
+  local expected = arguments[1][1] or arguments[1]
+  -- Handle cases where we're indeed checking for a real trailing newline.
+  local dedented = util.dedent(expected)
+  if dedented ~= expected then
+    expected = dedented:gsub('\n$', '')
+  end
+  return expected
+end
+
 --- Assert about the entire buffer contents.
 local function has_buf_contents(_, arguments)
-  local expected = arguments[1][1] or arguments[1]
   local bufnr = arguments[1].bufnr or 0
   local got = table.concat(vim.api.nvim_buf_get_lines(bufnr, 0, -1, false), '\n')
-  assert.is.equal(expected, got)
+  assert.is.equal(_expected(arguments), got)
   return true
 end
-
 assert:register('assertion', 'contents', has_buf_contents)
 
 --- Assert about the current infoview contents.
 local function has_infoview_contents(_, arguments)
-  local expected = util.dedent(arguments[1][1] or arguments[1])
+  local expected = _expected(arguments)
   local target_infoview = arguments[1].infoview or infoview.get_current_infoview()
   -- In Lean 3, the fileProgress notification is unreliable,
   -- so we may think we're done processing when we're actually not.
   -- This means that we'll sometimes get an empty response and then call it a day.
   -- To address this, we assume that we'll only assert
   -- nonempty contents in the Lean 3 tests, and retry updating the current pin
   -- until we get something.
-  if vim.opt.filetype:get() == "lean3" then
-    assert.are_not.same(expected, "")
+  if vim.opt.filetype:get() == 'lean3' then
+    assert.are_not.same(expected, '')
     local succeeded, _ = pcall(helpers.wait_for_loading_pins, target_infoview)
     local curr_pin = target_infoview.info.pin
 
@@ -243,30 +256,28 @@ local function has_infoview_contents(_, arguments)
       end
     end
 
-    assert.message("never got Lean 3 data").is_true(succeeded and #got ~= 0)
+    assert.message('never got Lean 3 data').is_true(succeeded and #got ~= 0)
   else
     helpers.wait_for_loading_pins(target_infoview)
   end
-  local got = table.concat(target_infoview:get_lines(), '\n')
-  assert.are.same(expected, got)
+  local got = table.concat(target_infoview:get_lines(), '\n'):gsub('\n$', '')
+  assert.is.equal(expected, got)
   return true
 end
 
 
 --- Assert about the current infoview contents without waiting for the pins to load.
 local function has_infoview_contents_nowait(_, arguments)
-  local expected = util.dedent(arguments[1][1] or arguments[1])
   local target_infoview = arguments[1].infoview or infoview.get_current_infoview()
   local got = table.concat(target_infoview:get_lines(), '\n')
-  assert.are.same(expected, got)
+  assert.are.same(_expected(arguments), got)
   return true
 end
 
 local function has_diff_contents(_, arguments)
-  local expected = util.dedent(arguments[1][1] or arguments[1])
   local target_infoview = arguments[1].infoview or infoview.get_current_infoview()
   local got = table.concat(target_infoview:get_diff_lines(), '\n')
-  assert.are.same(expected, got)
+  assert.are.same(_expected(arguments), got)
   return true
 end
 

lua/tests/helpers_spec.lua

@@ -0,0 +1,34 @@
+---@brief [[
+--- Tests for our own testing helpers.
+---@brief ]]
+
+local helpers = require('tests.helpers')
+
+describe('clean_buffer <-> assert.contents', function()
+  it('creates single line buffers', helpers.clean_buffer('foo bar', function()
+    assert.are.same(
+        vim.api.nvim_buf_get_lines(0, 0, -1, false), { 'foo bar' }
+    )
+    assert.contents.are('foo bar')
+  end))
+
+  it('creates multiline buffers', helpers.clean_buffer([[
+    foo
+    bar
+  ]], function()
+    assert.are.same(
+        vim.api.nvim_buf_get_lines(0, 0, -1, false), { 'foo', 'bar' }
+    )
+    assert.contents.are[[
+      foo
+      bar
+    ]]
+  end))
+
+  it('detects actual intended trailing newlines', helpers.clean_buffer('foo\n\n', function()
+    assert.are.same(
+        vim.api.nvim_buf_get_lines(0, 0, -1, false), { 'foo', '' }
+    )
+    assert.contents.are('foo\n')
+  end))
+end)

lua/tests/infoview/contents_spec.lua

@@ -37,21 +37,17 @@ describe('infoview content (auto-)update', function()
     -- In theory we don't care where we are, but the right answer changes
     assert.are.same(vim.api.nvim_win_get_cursor(0), {1, 0})
 
-    -- FIXME: Trailing extra newline.
     assert.infoview_contents.are[[
       ▶ 1:1-1:6: information:
       1
-
     ]]
   end)
 
   it('updates when the cursor moves', function()
     helpers.move_cursor{ to = {3, 0} }
-    -- FIXME: Trailing extra newline.
     assert.infoview_contents.are[[
       ▶ 3:1-3:6: information:
       9.000000
-
     ]]
   end)
 
@@ -64,14 +60,12 @@ describe('infoview content (auto-)update', function()
     assert.infoview_contents.are[[
       ▶ 3:1-3:6: information:
       9.000000
-
     ]]
 
     helpers.move_cursor{ to = {1, 0} }
     assert.infoview_contents.are[[
       ▶ 1:1-1:6: information:
       1
-
     ]]
 
     -- Now switch back to the other window and we see the original location...
@@ -80,7 +74,6 @@ describe('infoview content (auto-)update', function()
     assert.infoview_contents.are[[
       ▶ 3:1-3:6: information:
       9.000000
-
     ]]
 
     vim.api.nvim_win_close(second_window, false)
@@ -111,14 +104,12 @@ describe('infoview content (auto-)update', function()
     assert.infoview_contents.are[[
       ▶ 1:1-1:6: information:
       1
-
     ]]
 
     helpers.move_cursor{ to = {3, 0} }
     assert.infoview_contents.are[[
       ▶ 3:1-3:6: information:
       9.000000
-
     ]]
   end)
 
@@ -144,23 +135,20 @@ describe('infoview content (auto-)update', function()
       assert.infoview_contents.are[[
         ▶ 1:1-1:6: information:
         1
-
       ]]
 
       vim.cmd.tabnew(fixtures.project.path .. '/Test/Squares.lean')
       helpers.move_cursor{ to = {3, 0} }
       assert.infoview_contents.are[[
         ▶ 3:1-3:6: information:
         9.000000
-
       ]]
 
       -- But the first tab's contents are unchanged even without re-entering.
       assert.infoview_contents.are{
         [[
           ▶ 1:1-1:6: information:
           1
-
         ]],
         infoview = tab1_infoview
       }
@@ -177,14 +165,12 @@ describe('infoview content (auto-)update', function()
       assert.infoview_contents.are[[
         ▶ 3:1-3:6: information:
         9.000000
-
       ]]
 
       helpers.move_cursor{ to = {1, 0} }
       assert.infoview_contents.are[[
         ▶ 1:1-1:6: information:
         1
-
       ]]
 
       vim.cmd(tab2 .. 'tabclose')

lua/tests/infoview/pause_spec.lua

@@ -16,19 +16,15 @@ describe('infoview pause/unpause', function()
   it("can pause and unpause updates", function(_)
     vim.cmd('edit! ' .. fixtures.project.path .. '/Test/Squares.lean')
     helpers.move_cursor{ to = {3, 0} }
-    -- FIXME: Trailing extra newline.
     assert.infoview_contents.are[[
       ▶ 3:1-3:6: information:
       9.000000
-
     ]]
 
     helpers.move_cursor{ to = {1, 0} }
-    -- FIXME: Trailing extra newline.
     assert.infoview_contents.are[[
       ▶ 1:1-1:6: information:
       1
-
     ]]
 
     -- FIXME: Demeter is angry.
@@ -45,25 +41,20 @@ describe('infoview pause/unpause', function()
     assert.infoview_contents.are[[
       ▶ 1:1-1:6: information:
       1
-
     ]]
 
     -- Unpausing triggers an update.
     pin:unpause()
-    -- FIXME: Trailing extra newline.
     assert.infoview_contents.are[[
       ▶ 3:1-3:6: information:
       9.000000
-
     ]]
 
     -- And continued movement continues updating.
     helpers.move_cursor{ to = {1, 0} }
-    -- FIXME: Trailing extra newline.
     assert.infoview_contents.are[[
       ▶ 1:1-1:6: information:
       1
-
     ]]
   end)
 

lua/tests/infoview/pin_spec.lua

@@ -1,13 +1,12 @@
 ---@brief [[
 --- Tests for the placing of infoview pins.
 ---@brief ]]
-local dedent = require('lean._util').dedent
 local infoview = require('lean.infoview')
 local helpers = require('tests.helpers')
 
 require('lean').setup{ lsp = { enable = true } }
 
-describe('infoview pins', helpers.clean_buffer(dedent[[
+describe('infoview pins', helpers.clean_buffer([[
   theorem has_tactic_goal : p ∨ q → q ∨ p := by
     intro h
     cases h with

lua/tests/language_support_spec.lua

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

lua/tests/lean3/infoview/widgets_spec.lua

@@ -57,7 +57,6 @@ helpers.if_has_lean3('infoview widgets', clean_buffer('example : 2 = 2 := by ref
     infoview.enable_widgets()
     helpers.move_cursor{ to = {1, 22} }
     -- we're looking for `filter` as our widget
-    -- FIXME: Extra newline only with widgets enabled
     assert.infoview_contents.are[[
       filter: no filter
       ▶ 1 goal