Stream: jsCoq

Topic: Keybindings problem


view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2021 at 18:11):

I have indeed heard of similar reports

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 07:01 UTC