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

Improve :Telescope loogle #317

Open
1 of 3 tasks
hargoniX opened this issue Nov 6, 2023 · 1 comment
Open
1 of 3 tasks

Improve :Telescope loogle #317

hargoniX opened this issue Nov 6, 2023 · 1 comment
Labels
enhancement New feature or request

Comments

@hargoniX
Copy link
Collaborator

hargoniX commented Nov 6, 2023

As discussed in #316 we would like a few improvements:

  • being able to type unicode in the prompt. This requires hooking into the abbreviation framework
  • being able to use telescope for the search directly. This is a little more complicated as we don't want to spam the API with live updated input so we should probably add some debouncing to this feature.
  • automatically importing the declaration that is used. Once the LSP provides an "auto import" code action it should be possible to call this with the identifier in order to add the input if it is not yet present.
@hargoniX hargoniX added the enhancement New feature or request label Nov 6, 2023
@Julian
Copy link
Owner

Julian commented Nov 24, 2023

Another different path to think about I think is integrating with the workspace -- e..g maybe it'd be nice to have a Loogle searcher where it helps you assemble your query using current LSP workspace symbols.

(I'm purely dreaming up crude ideas here) but just like e.g. require('telescope.builtin').lsp_dynamic_workspace_symbols() will telescope over all the Lean stuff you're currently importing, perhaps it'd be nice to combine that with Loogle such that you could type a query like Re. ?a Re. and have telescope help you convert the Re to Real.sin (because you've imported that).

Obviously that starts to use some more complicated telescope functionality but I think something like that should be feasible (of course not saying it's urgent, but I like that we can collect ideas).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants