Add the command to toggle the virtual scrollbar to the palette

[jtpio]

References

This makes it easier to toggle the virtual scrollbar with the keyboard only.

Code changes

Add the notebook:toggle-virtual-scrollbar command to the command palette

User-facing changes

Before

After

Backwards-incompatible changes

None

[jupyterlab-probot]

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

[krassowski]

Should we adjust the label to "Toggle Virtual Scrollbar" when used from palette? Or maybe in general? In that case this would need to target 4.3.x to avoid breaking translations.

[jtpio]

Should we adjust the label to "Toggle Virtual Scrollbar" when used from palette? Or maybe in general? In that case this would need to target 4.3.x to avoid breaking translations.

It looks like other commands don't have the word "Toggle" in their label:

However some commands use the word "Show", such as "Show Line Numbers", which then uses a checkbox when the lines are displayed:

Would it make sense to do something similar for the virtual scrollbar?

[krassowski]

Yes, it makes sense yo me. It is more of a suggestion on making it easier for user to understand what this command is supposed to do, I do not want to block merging on this here, and if you wanted to backport this to 4.2.x the label could be adjusted in a follow up which would target 4.3.0

[jtpio]

Maybe there is no hurry to get this in a 4.2.x release and we can take the time to adjust the label correctly.

[krassowski]

Should we use getCurrent here for consistency?

Suggested change

	const current = tracker.currentWidget;
	const current = getCurrent(tracker, shell, args);

[jtpio]

I think this was the case at some point while iterating on this PR, but it was creating some issues because of the activate logic in that function, which was preventing switching to another widget in the dock panel:

jupyterlab/packages/notebook-extension/src/index.ts

Lines 2145 to 2149 in 56a0121

	const activate = args['activate'] !== false;
	if (activate && widget) {
	shell.activateById(widget.id);
	}

[krassowski]

Ok, thanks for the clarification!

[krassowski]

Thank you!