Add config for goals accomplished and no goals

Author: stephen-huan

lua/lean/config.lua

@@ -42,6 +42,8 @@
 ---@class lean.goal_markers.Config
 ---@field unsolved? string a character which will be placed on buffer lines where there is an unsolved goal
 ---@field accomplished? string a character which will be placed in the sign column of successful proofs
+---@field goals_accomplished? string a string to display in the infoview when the proof is successful
+---@field no_goals? string a string to display in the infoview when there are no active goals
 
 ---@class lean.infoview.Config
 ---@field mappings? { [string]: ElementEvent }
@@ -94,6 +96,8 @@ local DEFAULTS = {
   goal_markers = {
     unsolved = ' ⚒ ',
     accomplished = '🎉',
+    goals_accomplished = 'Goals accomplished 🎉',
+    no_goals = 'No goals.',
   },
 
   ---@type Log

lua/lean/infoview/components.lua

@@ -90,10 +90,11 @@ function components.goal_at(params, sess, use_widgets)
   end
 
   local title
+  local markers = config().goal_markers
   if lsp.goals_accomplished_at(params) then
-    title = 'Goals accomplished 🎉'
+    title = markers.goals_accomplished
   elseif goal and #goal == 0 then -- between goals / Lean <4.19 with no markers
-    title = vim.g.lean_no_goals_message or 'No goals.'
+    title = vim.g.lean_no_goals_message or markers.no_goals
   else
     return children, err
   end

lua/lean/lsp.lua

@@ -329,16 +329,17 @@ function lsp.enable(opts)
     },
     on_init = function(_, response)
       local version = response.serverInfo.version
+      local markers = config().goal_markers
       ---Lean 4.19 introduces silent diagnostics, which we use to differentiate
-      ---between "No goals." and "Goals accomplished. For older versions, we
+      ---between "No goals." and "Goals accomplished." For older versions, we
       ---always say the latter (which is consistent with `lean.nvim`'s historic
       ---behavior, albeit not with VSCode's).
       ---
       ---Technically this being a global is wrong, and will mean we start
       ---showing the wrong message if someone opens an older Lean buffer in the
       ---same session as a newer one...
-      vim.g.lean_no_goals_message = vim.version.ge(version, '0.3.0') and 'No goals.'
-        or 'Goals accomplished 🎉'
+      vim.g.lean_no_goals_message = vim.version.ge(version, '0.3.0') and markers.no_goals
+        or markers.goals_accomplished
     end,
   })
   require('lspconfig').leanls.setup(opts)