This adds JSON files to specify the human-readable name and description of hotkeys.
I use JSON files because that seems neater for extension/modders.
No need for C++ changes here, though it'd be nice to be able to react to hotloading .json
Open questions:
- Should I remove the hotkeys from the in-game manual?
Also clean up the code a tad.