Skip to content

Commit

Permalink
EXPERIMENTAL: Drop customizability of input method
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
mekeor committed Dec 6, 2024
1 parent 8e5923c commit 2ffaae7
Show file tree
Hide file tree
Showing 2 changed files with 1,786 additions and 2,101 deletions.
Loading

0 comments on commit 2ffaae7

Please sign in to comment.