From 94f6f8908560c2f378117c66093086a02fceb826 Mon Sep 17 00:00:00 2001 From: Mykola Morhun Date: Tue, 29 Oct 2019 12:13:46 +0000 Subject: [PATCH] Add terminal renderer option into terminal preferences Signed-off-by: Mykola Morhun --- .../src/browser/terminal-preferences.ts | 16 ++++++++++- .../src/browser/terminal-widget-impl.ts | 27 +++++++++++++++++-- 2 files changed, 40 insertions(+), 3 deletions(-) diff --git a/packages/terminal/src/browser/terminal-preferences.ts b/packages/terminal/src/browser/terminal-preferences.ts index ad4692e279ba1..7cd508729322a 100644 --- a/packages/terminal/src/browser/terminal-preferences.ts +++ b/packages/terminal/src/browser/terminal-preferences.ts @@ -68,7 +68,13 @@ export const TerminalConfigSchema: PreferenceSchema = { 'terminal.integrated.scrollback': { description: 'Controls the maximum amount of lines the terminal keeps in its buffer.', type: 'number', - default: 1000, + default: 1000 + }, + 'terminal.integrated.rendererType': { + description: 'Controls how the terminal is rendered.', + type: 'string', + enum: ['canvas', 'dom'], + default: 'canvas' } } }; @@ -83,10 +89,18 @@ export interface TerminalConfiguration { 'terminal.integrated.letterSpacing': number 'terminal.integrated.lineHeight': number, 'terminal.integrated.scrollback': number, + 'terminal.integrated.rendererType': TerminalRendererType } type FontWeight = 'normal' | 'bold' | '100' | '200' | '300' | '400' | '500' | '600' | '700' | '800' | '900'; +export type TerminalRendererType = 'canvas' | 'dom'; +export const DEFAULT_TERMINAL_RENDERER_TYPE = 'canvas'; +// tslint:disable-next-line:no-any +export function isTerminalRendererType(arg: any): arg is TerminalRendererType { + return typeof arg === 'string' && (arg === 'canvas' || arg === 'dom'); +} + export const TerminalPreferences = Symbol('TerminalPreferences'); export type TerminalPreferences = PreferenceProxy; diff --git a/packages/terminal/src/browser/terminal-widget-impl.ts b/packages/terminal/src/browser/terminal-widget-impl.ts index 3566e11207bbc..86ebb64f9885a 100644 --- a/packages/terminal/src/browser/terminal-widget-impl.ts +++ b/packages/terminal/src/browser/terminal-widget-impl.ts @@ -29,7 +29,7 @@ import { ThemeService } from '@theia/core/lib/browser/theming'; import { TerminalWidgetOptions, TerminalWidget } from './base/terminal-widget'; import { MessageConnection } from 'vscode-jsonrpc'; import { Deferred } from '@theia/core/lib/common/promise-util'; -import { TerminalPreferences } from './terminal-preferences'; +import { TerminalPreferences, TerminalRendererType, isTerminalRendererType, DEFAULT_TERMINAL_RENDERER_TYPE } from './terminal-preferences'; import { TerminalContribution } from './terminal-contribution'; import URI from '@theia/core/lib/common/uri'; import { TerminalService } from './base/terminal-service'; @@ -109,6 +109,7 @@ export class TerminalWidgetImpl extends TerminalWidget implements StatefulWidget letterSpacing: this.preferences['terminal.integrated.letterSpacing'], lineHeight: this.preferences['terminal.integrated.lineHeight'], scrollback: this.preferences['terminal.integrated.scrollback'], + rendererType: this.getTerminalRendererType(this.preferences['terminal.integrated.rendererType']), theme: { foreground: cssProps.foreground, background: cssProps.background, @@ -137,7 +138,17 @@ export class TerminalWidgetImpl extends TerminalWidget implements StatefulWidget const lastSeparator = change.preferenceName.lastIndexOf('.'); if (lastSeparator > 0) { const preferenceName = change.preferenceName.substr(lastSeparator + 1); - this.term.setOption(preferenceName, this.preferences[change.preferenceName]); + let preferenceValue = this.preferences[change.preferenceName]; + + if (preferenceName === 'rendererType') { + const newRendererType: string = this.preferences[change.preferenceName] as string; + if (newRendererType !== this.getTerminalRendererType(newRendererType)) { + // given terminal renderer type is not supported or invalid + preferenceValue = DEFAULT_TERMINAL_RENDERER_TYPE; + } + } + + this.term.setOption(preferenceName, preferenceValue); this.needsResize = true; this.update(); } @@ -191,6 +202,18 @@ export class TerminalWidgetImpl extends TerminalWidget implements StatefulWidget } } + /** + * Returns given renderer type if it is valid and supported or default renderer otherwise. + * + * @param terminalRendererType desired terminal renderer type + */ + private getTerminalRendererType(terminalRendererType?: string | TerminalRendererType): Xterm.RendererType { + if (terminalRendererType && isTerminalRendererType(terminalRendererType)) { + return terminalRendererType; + } + return DEFAULT_TERMINAL_RENDERER_TYPE; + } + showHoverMessage(x: number, y: number, message: string): void { this.hoverMessage.innerText = message; this.hoverMessage.style.display = 'inline';