Improve `:Telescope loogle`
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
- [x] 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.
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).