Shachar Itzhaky (May 11 2021 at 18:06): Shachar Itzhaky (May 11 2021 at 18:06):Has anyone encountered a problem where the keyboard bindings do not work? Specifically on a Mac.
Benjamin Pierce reported having nonfunctional keybindings; other functionality works fine, including navigating with the toolbar buttons. I was not able to reproduce it anywhere.
Emilio Jesús Gallego Arias (May 11 2021 at 18:11):I have indeed heard of similar reports
Emilio Jesús Gallego Arias (May 11 2021 at 18:11):should be not too hard to debug tho, as we could add an option to have codemirror write in the console for the corresponding kbg handler
Emilio Jesús Gallego Arias (May 11 2021 at 18:12):it could be well the case that @Benjamin Pierce did install some app that hooks on some keybindings for desktop management?
Emilio Jesús Gallego Arias (May 11 2021 at 18:12):I think also modern chrome versions do allow to hook for keyboard events in a pretty easy way from the debugger
Shachar Itzhaky (May 11 2021 at 18:38):Our keyboard event handler hooks to the document and does not even go through CodeMirror. However this issue https://github.com/jscoq/jscoq/issues/203 teaches us that CodeMirror does steal away some keys in certain scenarios.
Last updated: Oct 13 2024 at 01:02 UTC