doc-gen4 icon indicating copy to clipboard operation
doc-gen4 copied to clipboard

Input focus is stolen by left or right column

Open sgraf812 opened this issue 3 years ago • 1 comments

I often press space in my web browser to go a page down, and shift+space to go a page up. These shortcuts don't appear to be working on pages such as https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Basic.html#PartialOrder.lift when I previously clicked a link in either nav column to the left or to the right.

It's a small inconvenience, but I'd prefer it if the navbars wouldn't steal the "input focus" so that my browser always does the PageDn in the middle column.

sgraf812 avatar Nov 21 '22 13:11 sgraf812

I understand the inconvenience, but I'd be hesitant to change this. IMO, the left and right navbars should remain scrollable with the keyboard for accessibility reasons.

lynn avatar Sep 01 '25 11:09 lynn