Expose editor scrollbar options and react to them being updated

This commit is contained in:
Alex Dima 2021-07-01 16:14:13 +02:00
parent 8e16690b35
commit e07ae76bd2
No known key found for this signature in database
GPG key ID: 6E58D7B045760DA0
9 changed files with 119 additions and 25 deletions

View file

@ -48,7 +48,7 @@ export abstract class AbstractScrollbar extends Widget {
protected _scrollByPage: boolean;
private _lazyRender: boolean;
protected _scrollbarState: ScrollbarState;
private _visibilityController: ScrollbarVisibilityController;
protected _visibilityController: ScrollbarVisibilityController;
private _mouseMoveMonitor: GlobalMouseMoveMonitor<IStandardMouseMoveEventData>;
public domNode: FastDomNode<HTMLElement>;

View file

@ -107,4 +107,11 @@ export class HorizontalScrollbar extends AbstractScrollbar {
public writeScrollPosition(target: INewScrollPosition, scrollPosition: number): void {
target.scrollLeft = scrollPosition;
}
public updateOptions(options: ScrollableElementResolvedOptions): void {
this.updateScrollbarSize(options.horizontal === ScrollbarVisibility.Hidden ? 0 : options.horizontalScrollbarSize);
this._scrollbarState.setOppositeScrollbarSize(options.vertical === ScrollbarVisibility.Hidden ? 0 : options.verticalScrollbarSize);
this._visibilityController.setVisibility(options.horizontal);
this._scrollByPage = options.scrollByPage;
}
}

View file

@ -288,8 +288,6 @@ export abstract class AbstractScrollableElement extends Widget {
/**
* Update configuration options for the scrollbar.
* Really this is Editor.IEditorScrollbarOptions, but base shouldn't
* depend on Editor.
*/
public updateOptions(newOptions: ScrollableElementChangeOptions): void {
if (typeof newOptions.handleMouseWheel !== 'undefined') {
@ -305,9 +303,23 @@ export abstract class AbstractScrollableElement extends Widget {
if (typeof newOptions.scrollPredominantAxis !== 'undefined') {
this._options.scrollPredominantAxis = newOptions.scrollPredominantAxis;
}
if (typeof newOptions.horizontalScrollbarSize !== 'undefined') {
this._horizontalScrollbar.updateScrollbarSize(newOptions.horizontalScrollbarSize);
if (typeof newOptions.horizontal !== 'undefined') {
this._options.horizontal = newOptions.horizontal;
}
if (typeof newOptions.vertical !== 'undefined') {
this._options.vertical = newOptions.vertical;
}
if (typeof newOptions.horizontalScrollbarSize !== 'undefined') {
this._options.horizontalScrollbarSize = newOptions.horizontalScrollbarSize;
}
if (typeof newOptions.verticalScrollbarSize !== 'undefined') {
this._options.verticalScrollbarSize = newOptions.verticalScrollbarSize;
}
if (typeof newOptions.scrollByPage !== 'undefined') {
this._options.scrollByPage = newOptions.scrollByPage;
}
this._horizontalScrollbar.updateOptions(this._options);
this._verticalScrollbar.updateOptions(this._options);
if (!this._options.lazyRender) {
this._render();

View file

@ -131,7 +131,11 @@ export interface ScrollableElementChangeOptions {
mouseWheelScrollSensitivity?: number;
fastScrollSensitivity?: number;
scrollPredominantAxis?: boolean;
horizontal?: ScrollbarVisibility;
horizontalScrollbarSize?: number;
vertical?: ScrollbarVisibility;
verticalScrollbarSize?: number;
scrollByPage?: boolean;
}
export interface ScrollableElementResolvedOptions {

View file

@ -20,7 +20,7 @@ export class ScrollbarState {
* For the vertical scrollbar: the height of the pair horizontal scrollbar.
* For the horizontal scrollbar: the width of the pair vertical scrollbar.
*/
private readonly _oppositeScrollbarSize: number;
private _oppositeScrollbarSize: number;
/**
* For the vertical scrollbar: the height of the scrollbar's arrows.
@ -115,7 +115,11 @@ export class ScrollbarState {
}
public setScrollbarSize(scrollbarSize: number): void {
this._scrollbarSize = scrollbarSize;
this._scrollbarSize = Math.round(scrollbarSize);
}
public setOppositeScrollbarSize(oppositeScrollbarSize: number): void {
this._oppositeScrollbarSize = Math.round(oppositeScrollbarSize);
}
private static _computeValues(oppositeScrollbarSize: number, arrowSize: number, visibleSize: number, scrollSize: number, scrollPosition: number) {

View file

@ -13,6 +13,7 @@ export class ScrollbarVisibilityController extends Disposable {
private _visibleClassName: string;
private _invisibleClassName: string;
private _domNode: FastDomNode<HTMLElement> | null;
private _rawShouldBeVisible: boolean;
private _shouldBeVisible: boolean;
private _isNeeded: boolean;
private _isVisible: boolean;
@ -26,24 +27,37 @@ export class ScrollbarVisibilityController extends Disposable {
this._domNode = null;
this._isVisible = false;
this._isNeeded = false;
this._rawShouldBeVisible = false;
this._shouldBeVisible = false;
this._revealTimer = this._register(new TimeoutTimer());
}
public setVisibility(visibility: ScrollbarVisibility): void {
if (this._visibility !== visibility) {
this._visibility = visibility;
this._updateShouldBeVisible();
}
}
// ----------------- Hide / Reveal
private applyVisibilitySetting(shouldBeVisible: boolean): boolean {
public setShouldBeVisible(rawShouldBeVisible: boolean): void {
this._rawShouldBeVisible = rawShouldBeVisible;
this._updateShouldBeVisible();
}
private _applyVisibilitySetting(): boolean {
if (this._visibility === ScrollbarVisibility.Hidden) {
return false;
}
if (this._visibility === ScrollbarVisibility.Visible) {
return true;
}
return shouldBeVisible;
return this._rawShouldBeVisible;
}
public setShouldBeVisible(rawShouldBeVisible: boolean): void {
const shouldBeVisible = this.applyVisibilitySetting(rawShouldBeVisible);
private _updateShouldBeVisible(): void {
const shouldBeVisible = this._applyVisibilitySetting();
if (this._shouldBeVisible !== shouldBeVisible) {
this._shouldBeVisible = shouldBeVisible;

View file

@ -107,4 +107,13 @@ export class VerticalScrollbar extends AbstractScrollbar {
public writeScrollPosition(target: INewScrollPosition, scrollPosition: number): void {
target.scrollTop = scrollPosition;
}
public updateOptions(options: ScrollableElementResolvedOptions): void {
this.updateScrollbarSize(options.vertical === ScrollbarVisibility.Hidden ? 0 : options.verticalScrollbarSize);
// give priority to vertical scroll bar over horizontal and let it scroll all the way to the bottom
this._scrollbarState.setOppositeScrollbarSize(0);
this._visibilityController.setVisibility(options.vertical);
this._scrollByPage = options.scrollByPage;
}
}

View file

@ -145,6 +145,11 @@ export class EditorScrollbar extends ViewPart {
const fastScrollSensitivity = options.get(EditorOption.fastScrollSensitivity);
const scrollPredominantAxis = options.get(EditorOption.scrollPredominantAxis);
const newOpts: ScrollableElementChangeOptions = {
vertical: scrollbar.vertical,
horizontal: scrollbar.horizontal,
verticalScrollbarSize: scrollbar.verticalScrollbarSize,
horizontalScrollbarSize: scrollbar.horizontalScrollbarSize,
scrollByPage: scrollbar.scrollByPage,
handleMouseWheel: scrollbar.handleMouseWheel,
mouseWheelScrollSensitivity: mouseWheelScrollSensitivity,
fastScrollSensitivity: fastScrollSensitivity,

View file

@ -3101,22 +3101,61 @@ function _scrollbarVisibilityFromString(visibility: string | undefined, defaultV
class EditorScrollbar extends BaseEditorOption<EditorOption.scrollbar, InternalEditorScrollbarOptions> {
constructor() {
const defaults: InternalEditorScrollbarOptions = {
vertical: ScrollbarVisibility.Auto,
horizontal: ScrollbarVisibility.Auto,
arrowSize: 11,
useShadows: true,
verticalHasArrows: false,
horizontalHasArrows: false,
horizontalScrollbarSize: 12,
horizontalSliderSize: 12,
verticalScrollbarSize: 14,
verticalSliderSize: 14,
handleMouseWheel: true,
alwaysConsumeMouseWheel: true,
scrollByPage: false
};
super(
EditorOption.scrollbar, 'scrollbar',
EditorOption.scrollbar, 'scrollbar', defaults,
{
vertical: ScrollbarVisibility.Auto,
horizontal: ScrollbarVisibility.Auto,
arrowSize: 11,
useShadows: true,
verticalHasArrows: false,
horizontalHasArrows: false,
horizontalScrollbarSize: 12,
horizontalSliderSize: 12,
verticalScrollbarSize: 14,
verticalSliderSize: 14,
handleMouseWheel: true,
alwaysConsumeMouseWheel: true,
scrollByPage: false
'editor.scrollbar.vertical': {
type: 'string',
enum: ['auto', 'visible', 'hidden'],
enumDescriptions: [
nls.localize('scrollbar.vertical.auto', "The vertical scrollbar will be visible only when necessary."),
nls.localize('scrollbar.vertical.visible', "The vertical scrollbar will always be visible."),
nls.localize('scrollbar.vertical.fit', "The vertical scrollbar will always be hidden."),
],
default: 'auto',
description: nls.localize('scrollbar.vertical', "Controls the visibility of the vertical scrollbar.")
},
'editor.scrollbar.horizontal': {
type: 'string',
enum: ['auto', 'visible', 'hidden'],
enumDescriptions: [
nls.localize('scrollbar.horizontal.auto', "The horizontal scrollbar will be visible only when necessary."),
nls.localize('scrollbar.horizontal.visible', "The horizontal scrollbar will always be visible."),
nls.localize('scrollbar.horizontal.fit', "The horizontal scrollbar will always be hidden."),
],
default: 'auto',
description: nls.localize('scrollbar.horizontal', "Controls the visibility of the horizontal scrollbar.")
},
'editor.scrollbar.verticalScrollbarSize': {
type: 'number',
default: defaults.verticalScrollbarSize,
description: nls.localize('scrollbar.verticalScrollbarSize', "The width of the vertical scrollbar.")
},
'editor.scrollbar.horizontalScrollbarSize': {
type: 'number',
default: defaults.horizontalScrollbarSize,
description: nls.localize('scrollbar.horizontalScrollbarSize', "The height of the horizontal scrollbar.")
},
'editor.scrollbar.scrollByPage': {
type: 'boolean',
default: defaults.scrollByPage,
description: nls.localize('scrollbar.scrollByPage', "Controls whether clicks scroll by page or jump to click position.")
}
}
);
}