Is there an official recommendation for editors to input Lean unicode characters?

Question

As mentioned in another question, the way that VSCode and other editors implement unicode characters that cannot be typed directly from most keyboards is an editor feature.

As such, different editors could do it differently, so that for instance, $\varphi$ and $\phi$ could be entered as \varphi, \phi, the other way around, or something else.

But perhaps there is still an official recommendation on how editors should let you type unicode characters; or was a choice made to not make an official recommendation?

Answer 1

Because maintaining such a big list of Unicode abbreviations is annoying and none of the editor mode maintainers are interested in encouraging untransferrable abbreviations, as far as I know, all of the Lean editor modes just copy the abbreviations.json file (the VS Code plugin is the most popular, so new abbreviations usually land there first). In practice I haven't heard of divergence between editor abbreviations files ever being an issue.

So to the extent that there is an "official recommendation" to use the VS Code plugin for Lean, that comes with the bundled list of abbreviations, but users can also add their own abbreviations if they want.