let lnWidth := if st.config.showLineNumbers then 4 else 0
           let availableWidth := if w > lnWidth then w - lnWidth else 0

             | some s => (s, currentSt)

             | some (s, cachedScrollCol, cachedWidth) =>
               if cachedScrollCol == view.scrollCol.val && cachedWidth == availableWidth then
                 (s, currentSt)
               else
                 -- Cache miss; fall through to recompute.
                 match getLineFromBuffer buf lineIdx with
                 | some lineStr =>
                   let sub := lineStr.toRawSubstring.drop view.scrollCol.val
                   let dl := takeVisual sub availableWidth
                   let updatedBuf := { buf with cache := buf.cache.update lineIdx dl view.scrollCol.val availableWidth }
                   let s' := currentSt.updateCurrentWorkgroup fun wg =>
                     { wg with buffers := wg.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
                   (dl, s')
                 | none => ("", currentSt)

                 let lnWidth := if st.config.showLineNumbers then 4 else 0
                 let availableWidth := if w > lnWidth then w - lnWidth else 0

                 let updatedBuf := { buf with cache := buf.cache.update lineIdx dl }

                 let updatedBuf := { buf with cache := buf.cache.update lineIdx dl view.scrollCol.val availableWidth }

  lineMap : Lean.RBMap Row String compare

  -- Cache key includes scroll column and available width to avoid stale renders.
  lineMap : Lean.RBMap Row (String × Nat × Nat) compare

  def find (c : RenderCache) (r : Row) : Option String :=

  def find (c : RenderCache) (r : Row) : Option (String × Nat × Nat) :=

  def update (c : RenderCache) (r : Row) (s : String) : RenderCache :=
    { lineMap := c.lineMap.insert r s }

  def update (c : RenderCache) (r : Row) (s : String) (scrollCol : Nat) (availableWidth : Nat) : RenderCache :=
    { lineMap := c.lineMap.insert r (s, scrollCol, availableWidth) }

    buf.table.tree.lineBreaks + 1

    buf.table.lineCount

       -- Treat ESC + <char> as Alt combination when it's a single character and not CSI.
       match pending.toList with
       | ['\x1b', ch] =>
         if ch != '[' then
           ({ state with inputState := { state.inputState with pendingKeys := "" } }, [Key.alt ch])
         else
           ({ state with inputState := { state.inputState with pendingKeys := pending, lastInputTime := currentTime } }, [])
       | _ =>

  let state := { state with windowHeight := rows, windowWidth := cols }

  let resized := rows != state.windowHeight || cols != state.windowWidth
  let state := { state with windowHeight := rows, windowWidth := cols, dirty := state.dirty || resized }