search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
278 stars 27 forks source link

specify file extension for abbreviations #348

Closed chenson2018 closed 3 months ago

chenson2018 commented 3 months ago

This is my attempt to implement what was suggested on Zulip for allowing the lean.nvim abbreviations for other file extensions.

The usage here would be that you call something like require('lean.abbreviations').enable('*.tex', {}) to add a file extension. As I've not ever written much Lua or nvim plugins previously I'm not sure at all about what is considered idiomatic, so please give feedback as needed!

Julian commented 3 months ago

Awesome! Thanks a ton for giving this a shot. I'll take a closer look in a bit (likely tomorrow) -- at first glance it seems good! One additional thing you might try is to add a test to the spec file which tests this functionality.

You should mostly be able to copy a test that's there and simply create a file with some other file extension.

In order to run the tests locally you'll need just (brew install just on macOS if you're there) -- or otherwise you can just rely on GitHub actions running them, though it'll take a bit longer obviously. Ask if that's not specific enough help!

chenson2018 commented 3 months ago

I took a stab at the unit testing, making changes to the existing helper function set_unique_name_so_we_always_have_a_separate_fake_file to support different file extensions and copying over a test as suggested.

Julian commented 3 months ago

Awesome! I did that test modification in a slightly different way, but now merging! Thanks again, and let me know how this goes!

chenson2018 commented 3 months ago

I saw your follow up commit to the testing, that's much cleaner. Thanks!