Add config for goals accomplished and no goals

Author: stephen-huan

lsp/leanls.lua

@@ -217,15 +217,16 @@ return {
   },
   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,
 }

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 }
@@ -95,6 +97,8 @@ local DEFAULTS = {
   goal_markers = {
     unsolved = ' ⚒ ',
     accomplished = '🎉',
+    goals_accomplished = 'Goals accomplished 🎉',
+    no_goals = 'No goals.',
   },
 
   ---@type Log

lua/lean/infoview/components.lua

@@ -88,10 +88,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