Enable scrolling tabs in tab bar in main area

[krassowski]

References

Fixes #10305, depends on jupyterlab/lumino#297

TODO:

• decide on the minimum tab width or make it into a setting
• maybe reduce the scroll buttons
• add active and pressed style to the buttons

Code changes

Adds a setting allowing to enable scrolling of tabs.

User-facing changes

Users can scroll:

• by pressing the arrow buttons at the ends of tabs list (which only show up if the tab bar overflows)
• by using browser built-in scrolling (e.g. Shift + mouse wheel; shift needed as this is left-right scrolling)
• when dragging tabs by hovering over the arrow buttons

Backwards-incompatible changes

None

[jupyterlab-probot]

Thanks for making a pull request to jupyterlab!
To try out this branch on binder, follow this link:

[aiqc]

One thing to consider about width is the kernel status indicator:

it gets hidden when min width is too small

[krassowski]

The proposed positioning of scroll buttons < and > is as in Firefox. Having the buttons on the ends allows to designate these buttons as dual purpose: scrolling on click and scrolling on hover when dragging tabs.

The potential downsides of having buttons at the ends are:

• a mouse user might need to go back and forth between the edges of the screen (if they do not have a mouse wheel); however, we can expect that a sizable portion of JupyterLab users has the main area divided into multiple areas (as this is what distinguishes JupyterLab from Notebook), so the distance to be traversed will be on average much smaller than the width of the screen (and it is more likely that the scrolling will be needed when using multiple areas over a single area).
• a keyboard-only user might need to press tab multiple times to navigate to the button scrolling in the other direction; we could think about alleviating this by binding left and right arrows to these buttons (when tabbar is focused).

Chrome had tab scrolling and scrolling buttons for over a year now (since Chrome 88 from Dec 2020), but differently to Firefox it is disabled by default (and buttons are next to each other). Chrome allows to choose the min-width behaviour between:

• no min-width
• pinned tab width (which is basically the width of an icon + padding)
• "medium" width
• "large" width
• full size width

Firefox allows to set min-width in pixels (browser.tabs.tabMinWidth) and the default seems to be 76:

[ajbozarth]

I'll make time to take a look at this and the lumino PR before end of week

[ajbozarth]

Note: I left my review on the lumino PR