Julian / lean.nvim

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

feat: initial loogle client #316

Closed hargoniX closed 9 months ago

hargoniX commented 9 months ago

This is the initial version I hacked together yesterday, I've never written code for a bigger Neovim plugin so I don't quite know what quality standard we have here and how we want things to look and work?

Julian commented 9 months ago

Very nice, this looks like a great (and probably near mergeable) start!

As for standards -- perhaps you could add a few docstrings to the extension module, but otherwise seems pretty good to me! We use LuaLS type annotations -- the docs for those are here or should be cargo cultable from other functions in the plugin that you see.

Also, the tests will pass if you make the telescope dependency optional, which you can do by wrapping the require('telescope') in pcall so that we only enable the functionality when telescope is installed. Let me know if that isn't clear enough and I can put a suggestion on the code.

I'll leave one or two other small comments as I read through the code but yeah thanks again for sending!

hargoniX commented 9 months ago

Other possible improvements might be to have an alternate action in the telescope picker which also adds the imports (or maybe we should do that by default), or which only adds the imports? As I say I haven't used Loogle yet other than just trying it via your extension :), what's your take?

I don't think we should always add the import, we would have to determine if the thing is already imported (in particular transitive imports are a thing right now...) and in addition to that there might be some requirements on ordering etc. in the future. But I do agree it would be cool to have an additional action that gives you the thing + the import, I'll try to add that.

hargoniX commented 9 months ago

An additional thing I was wondering: Can we make it such that you can type unicode down there? Otherwise lots of math lemmas are out of reach for the vim search.

Julian commented 9 months ago

We do this to attach 2 autocmd events when entering command mode windows (q: and q/) for abbreviations.

If telescope fires a similar autocmd we can do the same, or else you can do it "manually" by binding those same few functions I think (convert and insert_char_pre) inside the Telescope typing buffer.

(This may be too vague, I haven't double checked anything concrete, but yeah I think this should be doable, maybe the above is enough to point you towards how)