The usual IDEs/editors for MMT (e.g. IntelliJ + MMT plugin or jEdit) feature an autocompletion feature for certain useful Unicode characters. For instance, I can type jle and immediately get suggested jleftrightarrow
that, upon autocompletion, is replaced by ↔
.
Is there a way to find out the reverse association? E.g. I have the symbol ☞
at hand and would like to know the autocompletion abbreviation starting with j
— if it exists. For that hand, I would get juri
.
The MMT OnlineTools I developed allow this: https://comfreek.github.io/mmteditor.
See screenshot below: if you already have a string full of Unicode symbols that you don't know how to type, just paste it under "how do I type X?". And if you are looking for a specific abbreviation — by Unicode character or by (parts of its) name — use the "abbreviation search" feature.
Internally, my tools pulls from (a copy of) the same resource file that Dennis linked in his answer.