Update terminal font family as soon as its updated

Fixes #6726
This commit is contained in:
Daniel Imms 2016-05-27 13:46:03 -07:00
parent 20f73da410
commit 3fde03980b

View file

@ -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<ITerminalConfiguration>();
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<ITerminalConfiguration>();
this.terminalDomElement.style.fontFamily = config.terminal.integrated.fontFamily;
}
public focus(): void {
this.focusTerminal(true);
}