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..c8317865 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, @@ -885,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, @@ -1084,10 +1086,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. -- @@ -1135,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 @@ -1192,7 +1197,36 @@ 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 current_uri = self.__position_params.textDocument.uri + 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. + 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..." 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 } + if self.__tick == tick and self.__info then + self.__info:render() + end + end + 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' 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/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) 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() 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 '' 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