vscode-lean4 abbreviation/unicode input engine as standalone

Stream: general

[Conner Bondurant]

I've found the abbreviation engine that the vscode extension utilizes to be a paradigm shift in the way it allows for accessing a far wider range of unicode symbols than are otherwise readily accessible by regular input methods. I'd love to have similar capability for general typing of notes or other features.

Are there any tools that are similar that work as more generalized IME layers for other contexts? or is there a possibility that the lean input system could be either broken out into a separate standalone tool, or maybe a setting that enables it in other non-lean files as well?

[Marc Huisinga]

Within VS Code, you can adjust the 'Lean 4: Input > Languages' setting to enable the abbreviation mechanism in other languages (e.g. Markdown). You may also find the manual entry helpful.

Outside of VS Code, there is unicode-input as a standalone TS library of the abbreviation logic and unicode-input-component as a standalone TS library for an input field that can be used on webpages (e.g. the search bar of Loogle or of the language reference).

[Conner Bondurant]

oh that sounds perfect

[Anthony Wang]

I recently made #general > Compose key sequences for Lean which works on Linux and probably also on Windows via WinCompose. This might be a bit different than what you're looking for though, since my script extracts only the sequences from the VSCode extension for use with other tools rather than the extension's input system itself.

[Conner Bondurant]

Well that also gives me another keyword that I wasn't aware of in the form of the compose key. So that'll probably be another avenue to explore as well.

[Patrick Massot]

Yet another possibility is to use https://github.com/OneDeadKey/kalamine to make your own keyboard layout full of math unicode symbols.