banacorn / agda-mode-vscode

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

Allow numeric input to complete ambiguous keyboard shortcuts #117

Open thorimur opened 2 years ago

thorimur commented 2 years ago

Some symbols are only accessible by browsing through a list of symbols. For example, to input ►, one types \t, is presented with a list of different triangles, then presses the right arrow key 6 times (or clicks the icon that appears). In emacs, my understanding is that one can simply type \t7 to select the seventh element of the list (►). It would be great to be able to do the same in VS Code!