In infoview, avoid computing #element.text when it might be vim.NIL#474
In infoview, avoid computing #element.text when it might be vim.NIL#474scott7z wants to merge 3 commits intoJulian:mainfrom
Conversation
scott7z
commented
Feb 7, 2026
scott7z
commented
This fixes tui.lua to avoid computing #element.text in some cases when
it might be vim.NIL, which is an error. In particular, CR on a symbol
in the infoview window will exercise this problem.
A new unit test checks that we no longer draw an error, and that the
right content is presented.
To reproduce by hand, edit
example (h: ∃ a:Nat, a = 3) := by apply h
and then CR on `a` in the info view.
Test with
just retest spec/infoview/tooltips_spec.lua
for more information, see https://pre-commit.ci
|
Hey! Can I confirm that you're on the latest version of lean.nvim when seeing this behavior? Specifically, the test here passes for me even before your change, other than that the expected infoview contents have trailing whitespace, which is something fixed awhile ago -- you can see that same failure here in CI at https://github.com/Julian/lean.nvim/actions/runs/21771149428/job/62818805876?pr=474#step:6:165 (though there's also a second test which unfortunately is just flaky). |
I forked from head, patched my change, and then sent the PR, so I think I was properly up to date. |
|
Do you also see the test passing even without your change? In my case your reproduction steps don't reproduce the issue. They do for you? |
I added a new test specifically to exercise the failures I was seeing. The pre-existing tooltips_spec didn't exercise the code path that was breaking, so it passed. However, I just remembered that I'm running nvim-nightly. Sure enough, it doesn't reproduce using nvim-0.11.6. Sorry for not checking that first! |
nvim has been getting more strict about converting JSON null to vim.NIL. In particular, a change to rpc.lua was made between 0.11.6 and nightly. https://github.com/neovim/neovim/blob/release-0.11/runtime/lua/vim/lsp/rpc.lua#L386 To support both versions, fields that might have been lua nil before now have to be checked against vim.NIL as well. This change checks for a null info_popup.doc early on, avoiding the downsteam checks in the previous commit.
|
It looks like nvim changed this behavior in That makes JSON null translate to vim.NIL instead of lua nil when doing JSON rpc. Based on that I've updated the patch, to check in a better place. |
| -- Recent versions of nvim translate JSON null to vim.NIL instead of | ||
| -- lua nil, so we have to check for both in rpc results. | ||
|
|
||
| if info_popup.exprExplicit ~= nil then |
There was a problem hiding this comment.
Seems like here might need investigating too
|
|
||
| if info_popup.exprExplicit ~= nil then | ||
| tooltip_element:add_child(InteractiveCode(info_popup.exprExplicit, sess, locations)) | ||
| if info_popup.type ~= nil then |
2 participants
