Unicode macros for Lean language

[bonsairobo]

It would significantly improve the experience of editing Lean code if Helix had support for unicode macros, like VSCode has, as described here:

The editor shares a number of features with Visual Studio Code; for example, you can type unicode characters with a backslash, so \and yields the unicode symbol for conjunction, and \a, \b, and \g yield the unicode α, β, and γ respectively.

The behavior present in the "lean4" vscode plugin is that you can just type "\a" and then <space> and the "\a" will be replaced with "α".

[pascalkuthe]

This could be either implemented using abbreviations (#1471) or unicode diagraph support (#1438). Both of which should be implemented using a future snippet system IMO.

This feature request is too specific, we don't adllow any language specific code in core.

[bonsairobo]

This feature request is too specific, we don't adllow any language specific code in core.

Sorry about that. I think I just put my request in the wrong place. I wasn't trying to imply that this should be implemented within "core."

[chtenb]

I personally use wincompose/xcompose for unicode input on windows/linux. The upside of this is that it also works the same way in any other application, like chat apps. Unicode input is not intrinsically a text editing problem, but rather a keyboard input problem.

[bonsairobo]

Thanks for the suggestion. I will try out xcompose.