Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
248 stars 25 forks source link

Fix the infoview containing a trailing newline in one case. #314

Closed Julian closed 10 months ago

Julian commented 10 months ago

It was when interactive diagnostics are present.

This is the main functional change of this commit -- but as part of it, the behavior of dedent as well as assert.contents and friends from the testing helpers have all changed to be what (to me) is more logical.

This is the case even though there's still one "magic" behavior (in a new helper function _expected) which seems required to get a test in the abbreviations spec to pass.

Also added here therefore are a bunch of tests for the testing helpers (and for dedent) which all pass and should help ensure that all this delicate code continues to work if it needs tweaking again.

A secondary tweak to the testing helpers is that assert.contents and friends now automatically dedent their expected value, which makes the tests a bit more prettily indented.

All the tests are then also refactored to use that "uniform" style for asserting against their contents, which is most of the whitespace change noise.