From 2a8847d1e80eef78940ae3e765d7cf1844487214 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Sat, 24 May 2025 17:43:27 -0400
Subject: [PATCH] Add config for goals accomplished and no goals

---
 lsp/leanls.lua                   | 7 ++++---
 lua/lean/config.lua              | 4 ++++
 lua/lean/infoview/components.lua | 5 +++--
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/lsp/leanls.lua b/lsp/leanls.lua
index dbdb0e51..68395c71 100644
--- a/lsp/leanls.lua
+++ b/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,
 }
diff --git a/lua/lean/config.lua b/lua/lean/config.lua
index 3fdf191f..0002672c 100644
--- a/lua/lean/config.lua
+++ b/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
diff --git a/lua/lean/infoview/components.lua b/lua/lean/infoview/components.lua
index 39e5ab7b..16341e2a 100644
--- a/lua/lean/infoview/components.lua
+++ b/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