leanprover-community
Rework Abbreviations for Input Method
Currently, our repository contains the abbreviations.json. I propose that it only contains an lean4-abbreviations.eld file that we build using an Elisp script.
I guess this can be regarded as upstream: https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json
I guess this can be regarded as upstream: https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json
The upstream URL has moved to a new location (see #97).
Maybe we should not use quail.el for abbreviations but abbrev.el mechanism instead. Let's check how easy it is to customize abbrev-tables, i.e. add or remove abbreviations, per directory-local variables or per user init.el customization etc.
If you define lean4-mode-abbrev-mode, it will be enabled by default when the user enables abbrev-mode. To make it opt-in, you can define a different variable and let the user set local-abbrev-table to its value as a local variable.
EDIT: The variable should be local-abbrev-table, and not abbrev-table.
I'm convinced that Abbrev tables are the appropriate approach for what lean4-eri implements as an ugly hack with Quail. But it's quite some work and not as important as other issues (like general refactoring and the aim of decoupling Lean4-Mode from lsp-mode, for sake of Eglot compatibility). That's why I will postpone it until a later milestone.