Fix the infoview containing a trailing newline in one case.

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)