Oh hello there. Another new release of lean.nvim is out, sneaking in just before 2025 🎊 📆.
It contains some additional autoindent fixes and better widget behavior for try this widgets.
Clickable Suggestions
Patrick Massot pointed out that in VSCode, when you see suggestions via e.g. the apply?, exact?, rw? tactics, that clicking in the infoview will perform the replacement.
Now this happens in nvim as well -- if you click on a suggestion, you should see the contents of your Lean source change.
Here's a quick demo if you haven't seen this feature before:
output.mp4
Note that "click" here has the same keybinding as other "clicking" operations in the infoview -- namely <CR> or K.
Telescope Picker for Abbreviations
I've also added a telescope picker for inserting abbreviations, which you can activate via :Telescope lean_abbreviations.
Here's how that looks:
telescope.mp4
This isn't a good replacement for \-based abbreviation entering -- not least of which because telescope has a bug that means that after inserting an abbreviation you end up in normal mode. But it's something we'd discussed previously as being cute if only to be able to dynamically see the list of abbreviations (and preview what they'll expand to), and can be improved upon slightly.
Other Changes
- Better dedenting autoindent behavior after some
sorrys and=>(though there's still one case I know is wrong) - The order of diagnostics and suggestions in the infoview has been flipped to match VSCode, with widgets now showing up first before diagnostics in the infoview.
I'd still love to hear any feedback on how well (or not well) autoindent is working for anyone, but I hope that the silence there is either everything working well or better everyone enjoying their holidays.
Until next time Neovim friends.
You should be able to update using whatever plugin manager you're using, e.g. via :Lazy update.
Full Changelog: v2024.12.1...v2024.12.2