Make RefreshComponent less twitchy via cancellation.

Author: Julian

lua/lean/tui.lua

@@ -551,6 +551,16 @@ function Element:render_lines(renderer)
     if element.__async_init and renderer then
       renderer.pending_elements[element] = true
       element.__async_init(function(resolved_element) ---@type Element resolved_element
+        -- Carry state (foldable open/close, RefreshComponent polling
+        -- cancellation, ...) from the prior resolved subtree to the new
+        -- one. Without this, every async frame would orphan whatever
+        -- `__state` handles lived in the previous subtree — most
+        -- noticeably leaking RefreshComponent polling loops that then
+        -- compound into a render storm.
+        local previous = element.__children[1]
+        if previous then
+          Element.transfer_state(previous, resolved_element)
+        end
         element:set_children { resolved_element }
         renderer.pending_elements[element] = nil
         renderer:render()

lua/lean/widgets/ProofWidgets/RefreshComponent.lua

@@ -7,28 +7,40 @@ local Html = require 'proofwidgets.html'
 ---
 --- Displays HTML that updates over time as a background Lean thread pushes
 --- new frames via the awaitRefresh RPC method.
+---
+--- A subtle point: each tree rebuild (cursor move, panel re-render, ...)
+--- creates a fresh RefreshComponent element with its own polling loop. If
+--- the previous element's loop is left running, every server frame it
+--- receives forces a full `renderer:render()` on the orphaned subtree,
+--- which compounds with every rebuild until the infoview is constantly
+--- re-rendering itself ("hourglass + flicker even when idle"). To avoid
+--- this we publish a `__state` cancel handle; `transfer_state` carries it
+--- to the new element which immediately cancels the old polling loop.
 ---@param ctx RenderContext
 ---@param props { state: table, cancelTk: table }
 ---@return Element
 return function(ctx, props)
+  local cancelled = false
+
   local element = Element:new {
     __async_init = function(rerender)
-      -- Start the monitor call (fire-and-forget).
-      -- It loops forever server-side and cancels the background computation
-      -- when the RPC session closes.
+      -- Start the monitor call (fire-and-forget). It loops forever server-side
+      -- and cancels the background computation when the RPC session closes.
       async.run(function()
         ctx:rpc_call('ProofWidgets.RefreshComponent.monitor', props)
       end)
 
-      -- Poll for new HTML frames.
+      -- Poll for new HTML frames. Bail as soon as a newer element has
+      -- adopted our position (via `__state`), otherwise the orphaned loop
+      -- would keep firing `renderer:render()` after every server frame.
       async.run(function()
         local idx = 0
-        while true do
+        while not cancelled do
           local response, err = ctx:rpc_call(
             'ProofWidgets.RefreshComponent.awaitRefresh',
             { state = props.state, oldIdx = idx }
           )
-          if err or not response then
+          if err or not response or cancelled then
             break
           end
           idx = response.idx
@@ -37,5 +49,17 @@ return function(ctx, props)
       end)
     end,
   }
+
+  element.__state = {
+    snapshot = function()
+      return function()
+        cancelled = true
+      end
+    end,
+    restore = function(_, cancel_previous)
+      cancel_previous()
+    end,
+  }
+
   return element
 end

spec/tui/core_spec.lua

@@ -599,6 +599,43 @@ describe('Element', function()
       assert.is.equal('▼ outer\n\n▶ inner', root:to_string())
     end)
 
+    it('transfers state across __async_init resolve callbacks', function()
+      -- Models what RefreshComponent needs: between successive resolutions
+      -- of an `__async_init`-driven element, state on the previous resolved
+      -- subtree (cancellation handles, foldable open-state, ...) must
+      -- transfer to the new one — otherwise nested stateful children
+      -- (e.g. RefreshComponent polling loops) get orphaned every frame.
+      local restored = {}
+      local function child_with_state(name)
+        local elem = Element:new { text = name }
+        elem.__state = {
+          snapshot = function()
+            return name
+          end,
+          restore = function(_, saved)
+            table.insert(restored, saved)
+          end,
+        }
+        return elem
+      end
+
+      local resolve
+      local async_elem = Element:new {
+        __async_init = function(rerender)
+          resolve = rerender
+        end,
+      }
+      local buffer = require('std.nvim.buffer').create { scratch = true, listed = false }
+      local renderer = async_elem:renderer { buffer = buffer }
+      renderer:render()
+
+      resolve(child_with_state 'a')
+      resolve(child_with_state 'b')
+      resolve(child_with_state 'c')
+
+      assert.are.same({ 'a', 'b' }, restored)
+    end)
+
     it('transfers state via a user-attached __state handle', function()
       -- Widgets without a built-in handle (foldables have one already) can
       -- opt into rebuild-survival by attaching a `__state` table with