Only show goal count for multiple goals.

Matches what vscode does, and is a bit less noisy.

lua/lean/infoview/components.lua

@@ -31,11 +31,13 @@ end
 function components.goal(goal)
   if type(goal) ~= "table" or not goal.goals then return {} end
 
-  local lines = {
-    #goal.goals == 0 and H('goals accomplished 🎉') or
-    #goal.goals == 1 and H('1 goal') or
-    H(string.format('%d goals', #goal.goals))
-  }
+  if #goal.goals == 0 then
+    return { H('goals accomplished 🎉') }
+  elseif #goal.goals == 1 then
+    return vim.split(goal.goals[1], '\n', true)
+  end
+
+  local lines = { H(string.format('%d goals', #goal.goals)) }
 
   for _, each in pairs(goal.goals) do
     vim.list_extend(lines, {''})

lua/tests/infoview/lsp_spec.lua

@@ -60,7 +60,7 @@ describe('infoview', function()
       -- hover for Lean 3 will also return information about `nat`, which is
       -- under the cursor, but we shouldn't count that as a goal.
       local text = infoview_lsp_update({3, 14})
-      assert.equal(text, '▶ 1 goal\n\n⊢ Type 1')
+      assert.equal(text, '⊢ Type 1')
     end)
   end)
 
@@ -79,7 +79,7 @@ describe('infoview', function()
     it('shows tactic state',
     function(_)
       local text = infoview_lsp_update({6, 9})
-      assert.has_all(text, {"1 goal", "p q : Prop", "h : p ∨ q", "⊢ q ∨ p"})
+      assert.has_all(text, {'p q : Prop', 'h : p ∨ q', "⊢ q ∨ p"})
     end)
   end)