In infoview, avoid computing #element.text when it might be vim.NIL

[scott7z]

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

[Julian]

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).

[scott7z]

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.

[Julian]

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?