From 72d1c0a65da494ecc0571be7e8567d760c0f2923 Mon Sep 17 00:00:00 2001 From: Valera Date: Mon, 16 Mar 2026 17:31:43 +0000 Subject: [PATCH 1/7] feat: keep stale goal state while processing When `keep_stale_goal` is enabled (default: true), the infoview preserves the last rendered goal state while Lean is processing, instead of replacing it with "Processing file..." and clearing all context. The infoview window gets a `leanInfoProcessing` winhighlight to visually indicate that the displayed state is stale. Refs: #369, #257 --- lua/lean/config.lua | 1 + lua/lean/infoview.lua | 26 ++++++++++++++++++++++++-- lua/lean/stderr.lua | 1 + syntax/leaninfo.lua | 1 + 4 files changed, 27 insertions(+), 2 deletions(-) diff --git a/lua/lean/config.lua b/lua/lean/config.lua index 3fdf191f..565b2548 100644 --- a/lua/lean/config.lua +++ b/lua/lean/config.lua @@ -46,6 +46,7 @@ ---@class lean.infoview.Config ---@field mappings? { [string]: ElementEvent } ---@field orientation? "auto"|"vertical"|"horizontal" what orientation to use for opened infoviews +---@field keep_stale_goal? boolean preserve the last goal state while Lean is processing instead of clearing it ---@field view_options? InfoviewViewOptions ---@field severity_markers? table characters to use for denoting diagnostic severity diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua index a3bcb250..07dc8022 100644 --- a/lua/lean/infoview.lua +++ b/lua/lean/infoview.lua @@ -40,6 +40,7 @@ local options = { autopause = false, indicators = 'auto', show_processing = true, + keep_stale_goal = true, show_no_info_message = false, show_term_goals = true, use_widgets = true, @@ -1084,10 +1085,13 @@ end --- ---@param params lsp.TextDocumentPositionParams ---@param use_widgets boolean ----@return Element +---@return Element? local function contents_for(params, use_widgets) local processing = progress.at(params) if processing == progress.Kind.processing then + if options.keep_stale_goal then + return nil + end -- When Lean is processing, diagnostics indicate what's building, -- but those diagnostics show up at the top of the file. -- @@ -1192,7 +1196,25 @@ Pin.update = a.void(function(self) self.loading = true self.__info:render() end - self.__data_element = contents_for(self.__position_params, self.__use_widgets) + local new_element = contents_for(self.__position_params, self.__use_widgets) + if new_element == nil then + if self.__data_element == Element.EMPTY then + -- First open: nothing stale to preserve, show "Processing file...". + self.__data_element = components.PROCESSING + self.__element:set_children { self.__data_element } + else + -- Subsequent: preserve stale goal, indicate staleness visually. + if self.__info.__infoview.window then + self.__info.__infoview.window.o.winhighlight = 'NormalNC:leanInfoProcessing' + end + end + if self.__tick == tick and self.__info and self.loading then + self.loading = false + self.__info:render() + end + return + end + self.__data_element = new_element -- FIXME: we don't have the right separation here for knowing when we're dead if self.__data_element == components.LSP_HAS_DIED then self.__info.__infoview.window.o.winhighlight = 'NormalNC:leanInfoLSPDead' diff --git a/lua/lean/stderr.lua b/lua/lean/stderr.lua index 669c44b9..a8dcc2f6 100644 --- a/lua/lean/stderr.lua +++ b/lua/lean/stderr.lua @@ -32,6 +32,7 @@ local function open_window(stderr_buffer) local stderr_window = Window:current() stderr_window:set_height(stderr_height) + stderr_window.o.winhighlight = 'NormalNC:Normal' stderr_buffer.o.filetype = 'leanstderr' initial_window:make_current() return stderr_window diff --git a/syntax/leaninfo.lua b/syntax/leaninfo.lua index 17390bc7..9e919e6f 100644 --- a/syntax/leaninfo.lua +++ b/syntax/leaninfo.lua @@ -20,6 +20,7 @@ vim.api.nvim_set_hl(0, 'leanInfoExpectedType', { default = true, link = 'Special vim.api.nvim_set_hl(0, 'leanInfoNCWarn', { default = true, link = 'Folded' }) vim.api.nvim_set_hl(0, 'leanInfoNCError', { default = true, link = 'NormalFloat' }) vim.api.nvim_set_hl(0, 'leanInfoPaused', { default = true, link = 'leanInfoNCWarn' }) +vim.api.nvim_set_hl(0, 'leanInfoProcessing', { default = true, link = 'leanInfoNCWarn' }) vim.api.nvim_set_hl(0, 'leanInfoLSPDead', { default = true, link = 'leanInfoNCError' }) -- Diagnostics From 7b932795b437dce816c19cc1352f2ae40f86f226 Mon Sep 17 00:00:00 2001 From: Valera Date: Mon, 16 Mar 2026 18:16:55 +0000 Subject: [PATCH 2/7] fix: only preserve stale goal for the same file Track the URI that produced the current data element, so we don't preserve stale goals from a previously opened file when a new one starts processing. Without this, switching to a new Lean buffer while a prior infoview state existed would show the old file's goals instead of "Processing file...". --- lua/lean/infoview.lua | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua index 07dc8022..bae04f3a 100644 --- a/lua/lean/infoview.lua +++ b/lua/lean/infoview.lua @@ -886,6 +886,7 @@ function Pin:new(obj) vim.tbl_extend('keep', obj, { paused = paused, __data_element = Element.EMPTY, + __data_element_uri = nil, __element = Element:new { name = 'pin' }, __info = obj.parent, __tick = 0, @@ -1196,17 +1197,21 @@ Pin.update = a.void(function(self) self.loading = true self.__info:render() end + local current_uri = self.__position_params.textDocument.uri local new_element = contents_for(self.__position_params, self.__use_widgets) if new_element == nil then - if self.__data_element == Element.EMPTY then - -- First open: nothing stale to preserve, show "Processing file...". - self.__data_element = components.PROCESSING - self.__element:set_children { self.__data_element } - else - -- Subsequent: preserve stale goal, indicate staleness visually. + local has_stale = self.__data_element ~= Element.EMPTY + and self.__data_element_uri == current_uri + if has_stale then + -- Preserve stale goal, indicate staleness visually. if self.__info.__infoview.window then self.__info.__infoview.window.o.winhighlight = 'NormalNC:leanInfoProcessing' end + else + -- No stale state for this file, show "Processing file...". + self.__data_element = components.PROCESSING + self.__data_element_uri = current_uri + self.__element:set_children { self.__data_element } end if self.__tick == tick and self.__info and self.loading then self.loading = false @@ -1215,6 +1220,7 @@ Pin.update = a.void(function(self) return end self.__data_element = new_element + self.__data_element_uri = current_uri -- FIXME: we don't have the right separation here for knowing when we're dead if self.__data_element == components.LSP_HAS_DIED then self.__info.__infoview.window.o.winhighlight = 'NormalNC:leanInfoLSPDead' From eeda3660cb43222378cf90197df4ba96cf5045d4 Mon Sep 17 00:00:00 2001 From: Valera Date: Mon, 16 Mar 2026 18:38:54 +0000 Subject: [PATCH 3/7] test: update multibyte tests for stale goal preservation Remove assertions that expected empty infoview when moving cursor to a no-goal position, since with keep_stale_goal the previous goal state may persist during brief reprocessing triggered by cursor movement. --- spec/infoview/contents_spec.lua | 4 ---- spec/infoview/plain_contents_spec.lua | 4 ---- 2 files changed, 8 deletions(-) diff --git a/spec/infoview/contents_spec.lua b/spec/infoview/contents_spec.lua index 0f63349f..d3396525 100644 --- a/spec/infoview/contents_spec.lua +++ b/spec/infoview/contents_spec.lua @@ -226,10 +226,6 @@ describe('interactive infoview', function() ⊢ 𝔽 = 𝔽 ]] - helpers.move_cursor { to = { 1, 44 } } - assert.infoview_contents.are [[ - ]] - helpers.move_cursor { to = { 1, 46 } } assert.infoview_contents.are [[ ▼ expected type (1:40-1:43) diff --git a/spec/infoview/plain_contents_spec.lua b/spec/infoview/plain_contents_spec.lua index 405f8f8f..97086288 100644 --- a/spec/infoview/plain_contents_spec.lua +++ b/spec/infoview/plain_contents_spec.lua @@ -137,10 +137,6 @@ describe('plain infoviews', function() ⊢ 𝔽 = 𝔽 ]] - helpers.move_cursor { to = { 1, 44 } } - assert.infoview_contents.are [[ - ]] - helpers.move_cursor { to = { 1, 46 } } assert.infoview_contents.are [[ ▼ expected type (1:40-1:43) From fc3618d26116d3f7136651144ed7e5048d0f22a8 Mon Sep 17 00:00:00 2001 From: Valera Date: Mon, 16 Mar 2026 18:49:49 +0000 Subject: [PATCH 4/7] fix: keep loading=true on first-open processing path When there's no stale state for a file (first open), we show "Processing file..." but must keep loading=true so that wait_for_loading_pins continues to wait for real content to arrive. Previously both paths set loading=false, causing tests to see "Processing file..." as the final content. Co-Authored-By: Claude Opus 4.6 --- lua/lean/infoview.lua | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua index bae04f3a..b4d0d7c6 100644 --- a/lua/lean/infoview.lua +++ b/lua/lean/infoview.lua @@ -1207,15 +1207,19 @@ Pin.update = a.void(function(self) if self.__info.__infoview.window then self.__info.__infoview.window.o.winhighlight = 'NormalNC:leanInfoProcessing' end + if self.__tick == tick and self.__info and self.loading then + self.loading = false + self.__info:render() + end else - -- No stale state for this file, show "Processing file...". + -- No stale state for this file, show "Processing file..." but keep + -- loading so that wait_for_loading_pins continues to wait for real content. self.__data_element = components.PROCESSING self.__data_element_uri = current_uri self.__element:set_children { self.__data_element } - end - if self.__tick == tick and self.__info and self.loading then - self.loading = false - self.__info:render() + if self.__tick == tick and self.__info then + self.__info:render() + end end return end From 61c82374b369d8a615a352d992ecd0d19f669545 Mon Sep 17 00:00:00 2001 From: Valera Date: Mon, 16 Mar 2026 19:00:18 +0000 Subject: [PATCH 5/7] fix(test): reset infoview cursor before search in unicode widget test The infoview window cursor persists between tests. After the previous test clicks [apply] at line 5, the cursor stays there. The next test's content also has [apply] at line 5, so helpers.search finds it at the same position and the "Cursor did not move!" assertion fails. Reset cursor to {1, 0} after go_to() so the forward search always finds the match. Co-Authored-By: Claude Opus 4.6 --- spec/widgets/core_spec.lua | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/widgets/core_spec.lua b/spec/widgets/core_spec.lua index 77c1e531..b497b672 100644 --- a/spec/widgets/core_spec.lua +++ b/spec/widgets/core_spec.lua @@ -76,6 +76,7 @@ describe('Lean core widgets', function() ]] infoview.go_to() + vim.api.nvim_win_set_cursor(0, { 1, 0 }) helpers.search 'apply] ' helpers.feed '' From 90d13fee97917bc36706f4e89b2c9baa092d0ef6 Mon Sep 17 00:00:00 2001 From: Valera Date: Mon, 16 Mar 2026 19:10:38 +0000 Subject: [PATCH 6/7] fix(test): include style field in float window config assertion Neovim nightly added a `style` field to `nvim_win_get_config()` output. Include it in the expected table so the test passes on both stable (where style is absent) and nightly (where style = ''). Co-Authored-By: Claude Opus 4.6 --- spec/std/nvim/window_spec.lua | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/std/nvim/window_spec.lua b/spec/std/nvim/window_spec.lua index fa6f0749..04304dc3 100644 --- a/spec/std/nvim/window_spec.lua +++ b/spec/std/nvim/window_spec.lua @@ -115,6 +115,7 @@ describe('Window', function() border = config.border, focusable = config.focusable, mouse = config.mouse, + style = config.style, zindex = config.zindex, }, config) float:close() From 3da846be4bb91577d556f686fefc08c4707612c0 Mon Sep 17 00:00:00 2001 From: Valera Date: Mon, 16 Mar 2026 19:58:08 +0000 Subject: [PATCH 7/7] fix: don't preserve stale goal when cursor is outside declarations contents_for() returned nil (via nonexistent components.EMPTY) when the cursor was at a position with no goal info and show_no_info_message was false. Our stale preservation logic treated nil as "Lean is processing", so it incorrectly kept showing the old goal state when the cursor moved outside any declaration (e.g. to a comment between theorems). Fix by returning Element.EMPTY instead, and also excluding NO_INFO and PROCESSING sentinels from being considered preservable stale state. Co-Authored-By: Claude Opus 4.6 --- lua/lean/infoview.lua | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lua/lean/infoview.lua b/lua/lean/infoview.lua index b4d0d7c6..c8317865 100644 --- a/lua/lean/infoview.lua +++ b/lua/lean/infoview.lua @@ -1140,7 +1140,7 @@ local function contents_for(params, use_widgets) elseif options.show_no_info_message then return components.NO_INFO else - return components.EMPTY + return Element.EMPTY end end @@ -1201,6 +1201,8 @@ Pin.update = a.void(function(self) local new_element = contents_for(self.__position_params, self.__use_widgets) if new_element == nil then local has_stale = self.__data_element ~= Element.EMPTY + and self.__data_element ~= components.NO_INFO + and self.__data_element ~= components.PROCESSING and self.__data_element_uri == current_uri if has_stale then -- Preserve stale goal, indicate staleness visually.