Rework Abbreviations for Input Method #93
Milestone
Comments
|
I guess this can be regarded as upstream: https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json |
mekeor
added a commit
that referenced
this issue
Dec 6, 2024
Fixes issue #93 "Rework Abbreviations for Input Method" (#93). This is an experimental commit. It's not yet decided if we'll implement it as such. There's an ongoing survey if anyone uses the customizability features of Lean4 input method. - Delete data/abbreviations.json. - Hard-code all quail rules into lean4-input.el directly. - Drop all complexity of lean4-input.el. - Drop copyright notice from agda-input.el in lean4-input.el because it's not based on it anymore. - Use "Lean4" as name for input method. - Use "L4" as abbreviation for the input method in the mode line so that it's different from Lean(3)-Mode.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Currently, our repository contains the
abbreviations.json. I propose that it only contains anlean4-abbreviations.eldfile that we build using an Elisp script.The text was updated successfully, but these errors were encountered: