Extract abbreviations functionality so that other languages can use it as well

[clason]

For example, Julia REPL supports entering Unicode chars via, e.g., \alpha -> α or \:beer: -> 🍺, which looks quite similar to Lean.

(You can see a full list here, which is generated from https://github.com/nvim-telescope/telescope-symbols.nvim/blob/master/script/julia_symbols.jl.)

Also see: https://github.com/GoldsteinE/compe-latex-symbols

[clason]

Also, any interest in adding https://github.com/L3MON4D3/LuaSnip support?

[Julian]

I've seen LuaSnip but not tried it myself -- definitely open to adding it though yeah.

(And yeah like I said definitely happy to extract this piece too, though it'll take a bit of generalizing I think, but yeah it's a good idea!)

[clason]

The thought occurs that this (Unicode input) is a relatively common task, and that vim already has a similar feature: digraphs. Maybe the way to go here is to add some tooling around that (for loading custom, filetype dependent, digraphs, better input suggestions/previews)?

[Julian]

I think that's quite interesting!

I'm aware of digraphs but I've essentially never used them myself even before this plugin (for some of the reasons you mentioned -- worst of which is the input suggestion thing, where if you type stuff you have no idea what you typed already, which symbol you're on the way to, etc.)

We'd need upstream changes though obviously -- probably that's part of what you're suggesting right? If so could definitely do some thinking about what that'd look like, I think the list you just gave is a pretty decent one on stuff that'd be needed, along with maybe being able to configure how to enter digraph entry mode (e.g. here we need it super often and want to trigger it with \ rather than reaching for c-k).

[clason]

I'm aware of digraphs but I've essentially never used them myself even before this plugin (for some of the reasons you mentioned -- worst of which is the input suggestion thing, where if you type stuff you have no idea what you typed already, which symbol you're on the way to, etc.)

Same here...

We'd need upstream changes though obviously -- probably that's part of what you're suggesting right? If so could definitely do some thinking about what that'd look like, I think the list you just gave is a pretty decent one on stuff that'd be needed, along with maybe being able to configure how to enter digraph entry mode (e.g. here we need it super often and want to trigger it with \ rather than reaching for c-k).

Yes, the hooks for digraph would have to go upstream (maybe even to vim?) Also agreed on exposing that feature so it's mappable/triggerable from a script.

It's probably not going to be a full replacement for autocomplete or snippet UX, but it's interesting as a sort of "vim-sneak for unicode"...

[clason]

If one were to go down that route, it might make sense to even generalize this to "ngraphs" (which may short-circuit) -- this way you can actually type alpha? (But this starts to sound like a completely different feature...)

Actually, a new complete mode ("symbols", <c-x><c-s>?) might be a more appropriate...

And there's also iabbrev (which however doesn't work (easily) with leading backslashes...), which (as abbrev) also easily works on the command line.

[clason]

Yeah, the more I think about it, the more abbrev sounds like what would be easiest to (ab)use. Just needs a good preview :)

[ram02z]

If anyone wants the abbreviations in vscode format for luasnip etc.

https://github.com/ram02z/dotfiles/blob/7429b91a601e0efa4a889b5cd16ec697c8139850/dot_config/nvim/snippets/maths_abbr.json

[Julian]

Before this repo, I had something which did that essentially. It live(d) here https://github.com/Julian/lean-unicode.vim/

[Julian]

Ups, hit space bar which GitHub decided to focus on the "Close with comment button"...

But yeah the above was a previous attempt -- we can do better than both I think (which is what Christian was requesting)