From 3fde03980baf7d33d14c36dce623ad1c89470d93 Mon Sep 17 00:00:00 2001 From: Daniel Imms Date: Fri, 27 May 2016 13:46:03 -0700 Subject: [PATCH] Update terminal font family as soon as its updated Fixes #6726 --- .../electron-browser/terminalPanel.ts | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/vs/workbench/parts/terminal/electron-browser/terminalPanel.ts b/src/vs/workbench/parts/terminal/electron-browser/terminalPanel.ts index 6c9b2729ea8..85b59f656c3 100644 --- a/src/vs/workbench/parts/terminal/electron-browser/terminalPanel.ts +++ b/src/vs/workbench/parts/terminal/electron-browser/terminalPanel.ts @@ -209,28 +209,35 @@ export class TerminalPanel extends Panel { } })); this.toDispose.push(this.themeService.onDidThemeChange((themeId) => { - this.setTerminalTheme(themeId); + this.setTerminalTheme(); + })); + this.toDispose.push(this.configurationService.onDidUpdateConfiguration((e) => { + this.setTerminalFont(); })); this.terminal.open(this.terminalDomElement); this.parentDomElement.appendChild(terminalScrollbar.getDomNode()); - let config = this.configurationService.getConfiguration(); - this.terminalDomElement.style.fontFamily = config.terminal.integrated.fontFamily; - this.setTerminalTheme(this.themeService.getTheme()); + this.setTerminalFont(); + this.setTerminalTheme(); resolve(void 0); }); } - private setTerminalTheme(themeId: string) { + private setTerminalTheme() { if (!this.terminal) { return; } - let baseThemeId = getBaseThemeId(themeId); + let baseThemeId = getBaseThemeId(this.themeService.getTheme()); this.terminal.colors = DEFAULT_ANSI_COLORS[baseThemeId]; this.terminal.refresh(0, this.terminal.rows); } + private setTerminalFont() { + let config = this.configurationService.getConfiguration(); + this.terminalDomElement.style.fontFamily = config.terminal.integrated.fontFamily; + } + public focus(): void { this.focusTerminal(true); } -- GitLab