banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

`asset/keymap.js` is outdated/incomplete compared to Agda's emacs-mode #171

Closed fredrik-bakke closed 8 months ago

fredrik-bakke commented 9 months ago

For example = maps to the fullwidth equals sign in emacs-mode but this symbol is not in asset/keymap.js. How was this file originally generated? Would it be easy to update it?

favonia commented 9 months ago

@fredrik-bakke @L-TChen For people who are interested, the asset is simply a finite state machine. So, for F=, you should find the "F" property at the top-level object, and then find the "=" property at the next level, and finally point ">>" (the "ending" symbol for this finite state machine) to a list containing the string .

banacorn commented 8 months ago

https://github.com/banacorn/keymap This is how the keymap was generated hehe

banacorn commented 8 months ago

This latest agda-input.el should now be included in asset/keymap.js

fredrik-bakke commented 8 months ago

Thanks a bunch!