development/vscode
development/vscode
1
0
Fork 0
mirror of https://github.com/Microsoft/vscode synced 2024-09-13 13:46:13 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fixes #142595: Correctly remove media query list listener

Browse source
This commit is contained in:
Alex Dima 2022-02-15 17:20:07 +01:00
parent 8dcfb37475
commit bd465c03ef
No known key found for this signature in database
GPG key ID: 39563C1504FDD0C9
1 changed files with 38 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
src/vs/base/browser/browser.ts
View file

@ -51,13 +51,45 @@ class WindowManager {
}
}
/**
* See https://developer.mozilla.org/en-US/docs/Web/API/Window/devicePixelRatio#monitoring_screen_resolution_or_zoom_level_changes
*/
class DevicePixelRatioMonitor extends Disposable {
private readonly _onDidChange = this._register(new Emitter<void>());
public readonly onDidChange = this._onDidChange.event;
private readonly _listener: () => void;
private _mediaQueryList: MediaQueryList | null;
constructor() {
super();
this._listener = () => this._handleChange(true);
this._mediaQueryList = null;
this._handleChange(false);
}
private _handleChange(fireEvent: boolean): void {
if (this._mediaQueryList) {
this._mediaQueryList.removeEventListener('change', this._listener);
}
this._mediaQueryList = matchMedia(`(resolution: ${window.devicePixelRatio}dppx)`);
this._mediaQueryList.addEventListener('change', this._listener);
if (fireEvent) {
this._onDidChange.fire();
}
}
}
class PixelRatioImpl extends Disposable {
private readonly _onDidChange = this._register(new Emitter<number>());
public readonly onDidChange = this._onDidChange.event;
private _value: number;
private _removeListener: () => void;
public get value(): number {
return this._value;
@ -67,28 +99,12 @@ class PixelRatioImpl extends Disposable {
super();
this._value = this._getPixelRatio();
this._removeListener = this._installResolutionListener();
}
public override dispose() {
this._removeListener();
super.dispose();
}
private _installResolutionListener(): () => void {
// See https://developer.mozilla.org/en-US/docs/Web/API/Window/devicePixelRatio#monitoring_screen_resolution_or_zoom_level_changes
const mediaQueryList = matchMedia(`(resolution: ${window.devicePixelRatio}dppx)`);
const listener = () => this._updateValue();
mediaQueryList.addEventListener('change', listener);
return () => {
mediaQueryList.removeEventListener('change', listener);
};
}
private _updateValue(): void {
this._value = this._getPixelRatio();
this._onDidChange.fire(this._value);
this._removeListener = this._installResolutionListener();
const dprMonitor = this._register(new DevicePixelRatioMonitor());
this._register(dprMonitor.onDidChange(() => {
this._value = this._getPixelRatio();
this._onDidChange.fire(this._value);
}));
}
private _getPixelRatio(): number {