Web editor interferes with browser shortcut

Stream: lean4

[Julian Berman]

On macOS (+Firefox), the editor https://live.lean-lang.org will interfere with at least the Cmd-L browser shortcut, which should take you to the address bar. I don't recall this always being the case (but I can't say I've used it a ton yet). Perhaps on windows this is also the case with Ctrl+L if someone cares to confirm. Is this behavior considered undesirable? (I honestly find it so undesirable that I'd like to check whether it's possible to never allow any website to quash a shortcut like that, but I'm also the sort of person that absolutely hates keyboard shortcuts on websites).

[Julian Berman]

(The behavior occurs only when the editor is focused of course, not if you click on the infoview or something.)

[Jon Eugster]

I believe this is the Lean4 vscode extension code binding this shortcut. I dont think lean4web actively sets any shortcuts bit it leverages basically all code of the vscode extension to work in a web context.

I wouldnt say this is actively desired; if there's a way to disable shortcuts (in lean4web's code) without modifying the Lean-extension code itself, that could be an option. I wont have the time to investigate myself for some time unfortunately.

[Marc Huisinga]

Jon Eugster said:

I believe this is the Lean4 vscode extension code binding this shortcut. I dont think lean4web actively sets any shortcuts bit it leverages basically all code of the vscode extension to work in a web context.

I wouldnt say this is actively desired; if there's a way to disable shortcuts (in lean4web's code) without modifying the Lean-extension code itself, that could be an option. I wont have the time to investigate myself for some time unfortunately.

vscode-lean4 does not set a Ctrl+L shortcut: https://github.com/leanprover/vscode-lean4/blob/7df64fb8e7eb9fd8910ce5381db09737d7eb79fe/vscode-lean4/package.json#L411

[Mac Malone]

VSCode itself, however, does set a Ctrl+L shortcut for selecting the current line: https://code.visualstudio.com/shortcuts/keyboard-shortcuts-windows.pdf

[Julian Berman]

The Monaco bug tracker has various discussions of how to get it to not do that for Monaco, I'm trying to figure out the current best way.