diff --git a/src/vs/workbench/contrib/terminal/browser/terminalConfigurationService.ts b/src/vs/workbench/contrib/terminal/browser/terminalConfigurationService.ts index 326d159c07829..93d0e090056b6 100644 --- a/src/vs/workbench/contrib/terminal/browser/terminalConfigurationService.ts +++ b/src/vs/workbench/contrib/terminal/browser/terminalConfigurationService.ts @@ -120,7 +120,7 @@ export class TerminalFontMetrics extends Disposable { const editorConfig = this._configurationService.getValue('editor'); let fontFamily = this._terminalConfigurationService.config.fontFamily || editorConfig.fontFamily || EDITOR_FONT_DEFAULTS.fontFamily || 'monospace'; - let fontSize = clampInt(this._terminalConfigurationService.config.fontSize, FontConstants.MinimumFontSize, FontConstants.MaximumFontSize, EDITOR_FONT_DEFAULTS.fontSize); + let fontSize = clampFloat(this._terminalConfigurationService.config.fontSize, FontConstants.MinimumFontSize, FontConstants.MaximumFontSize, EDITOR_FONT_DEFAULTS.fontSize); // Work around bad font on Fedora/Ubuntu if (!this._terminalConfigurationService.config.fontFamily) { @@ -131,7 +131,7 @@ export class TerminalFontMetrics extends Disposable { fontFamily = '\'Ubuntu Mono\''; // Ubuntu mono is somehow smaller, so set fontSize a bit larger to get the same perceived size. - fontSize = clampInt(fontSize + 2, FontConstants.MinimumFontSize, FontConstants.MaximumFontSize, EDITOR_FONT_DEFAULTS.fontSize); + fontSize = clampFloat(fontSize + 2, FontConstants.MinimumFontSize, FontConstants.MaximumFontSize, EDITOR_FONT_DEFAULTS.fontSize); } } @@ -256,4 +256,15 @@ function clampInt(source: string | number, minimum: number, maximum: number, } return clamp(r, minimum, maximum); } + +function clampFloat(source: string | number, minimum: number, maximum: number, fallback: T): number | T { + if (source === null || source === undefined) { + return fallback; + } + const r = isString(source) ? parseFloat(source) : source; + if (isNaN(r)) { + return fallback; + } + return clamp(r, minimum, maximum); +} // #endregion Utils diff --git a/src/vs/workbench/contrib/terminal/test/browser/terminalConfigurationService.test.ts b/src/vs/workbench/contrib/terminal/test/browser/terminalConfigurationService.test.ts index 206b113186ca2..e33b61508c51e 100644 --- a/src/vs/workbench/contrib/terminal/test/browser/terminalConfigurationService.test.ts +++ b/src/vs/workbench/contrib/terminal/test/browser/terminalConfigurationService.test.ts @@ -186,6 +186,53 @@ suite('Workbench - TerminalConfigurationService', () => { strictEqual(terminalConfigurationService.getFont(getActiveWindow()).fontSize, EDITOR_FONT_DEFAULTS.fontSize, 'The default editor font size should be used when terminal.integrated.fontSize is not set'); }); + test('fontSize 11.5 (decimal)', () => { + const terminalConfigurationService = createTerminalConfigationService({ + editor: { + fontFamily: 'foo', + fontSize: 9 + }, + terminal: { + integrated: { + fontFamily: 'bar', + fontSize: 11.5 + } + } + }); + strictEqual(terminalConfigurationService.getFont(getActiveWindow()).fontSize, 11.5, 'terminal.integrated.fontSize should preserve decimal values'); + }); + + test('fontSize 13.25 (decimal)', () => { + const terminalConfigurationService = createTerminalConfigationService({ + editor: { + fontFamily: 'foo', + fontSize: 9 + }, + terminal: { + integrated: { + fontFamily: 'bar', + fontSize: 13.25 + } + } + }); + strictEqual(terminalConfigurationService.getFont(getActiveWindow()).fontSize, 13.25, 'terminal.integrated.fontSize should preserve decimal values like 13.25'); + }); + + test('fontSize decimal (Linux Ubuntu)', () => { + const terminalConfigurationService = createTerminalConfigationService({ + editor: { + fontFamily: 'foo' + }, + terminal: { + integrated: { + fontFamily: null, + fontSize: 10.5 + } + } + }, LinuxDistro.Ubuntu); + strictEqual(terminalConfigurationService.getFont(getActiveWindow()).fontSize, 12.5, 'Ubuntu font size adjustment should preserve decimal values (10.5 + 2 = 12.5)'); + }); + test('lineHeight 2', () => { const terminalConfigurationService = createTerminalConfigationService({ editor: {