Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: initial loogle client #316

Merged
merged 7 commits into from
Nov 6, 2023
Merged

feat: initial loogle client #316

merged 7 commits into from
Nov 6, 2023

Conversation

hargoniX
Copy link
Collaborator

@hargoniX hargoniX commented Nov 6, 2023

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
Copy link
Owner

Julian commented Nov 6, 2023

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!

Copy link
Owner

@Julian Julian left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some minor comments but yeah looks nice!

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?

lua/telescope/_extensions/loogle/loogle_search.lua Outdated Show resolved Hide resolved
lua/telescope/_extensions/loogle/loogle_search.lua Outdated Show resolved Hide resolved
hargoniX and others added 2 commits November 6, 2023 18:12
Co-authored-by: Julian Berman <Julian@GrayVines.com>
@hargoniX
Copy link
Collaborator Author

hargoniX commented Nov 6, 2023

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
Copy link
Collaborator Author

hargoniX commented Nov 6, 2023

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
Copy link
Owner

Julian commented Nov 6, 2023

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)

Copy link
Owner

@Julian Julian left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great!

There's extra stuff we can add, like adding imports or unicode abbreviation support for the input prompt, but as a first version it's perfect!

Can you just add a line to the README mentioning this exists (maybe next to the current_search_paths telescope note), and maybe a screenshot to the wiki as well?

After that LGTM, feel free to merge, you've now got the power.

README.rst Outdated
@@ -81,6 +82,9 @@ Features
live grepping.
See the wiki for `a sample configuration <https://github.com/Julian/lean.nvim/wiki/Configuring-&-Extending#live-grep>`_.

* If `telescope.nvim <https://github.comnvim-telescope/telescope.nvim>`_ is present a `:Telescope loogle` command
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Minor typos, and an extra _ will make the nonsense cryptic reST error go away:

Suggested change
* If `telescope.nvim <https://github.comnvim-telescope/telescope.nvim>`_ is present a `:Telescope loogle` command
* If `telescope.nvim <https://github.com/nvim-telescope/telescope.nvim>`__ is present a `:Telescope loogle` command is available as a frontend for the `Loogle <https://loogle.lean-lang.org>`_ JSON API.

@hargoniX hargoniX merged commit 467f543 into Julian:main Nov 6, 2023
7 checks passed
@hargoniX hargoniX mentioned this pull request Nov 6, 2023
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants