Merge branch 'master' into parser_colon_notation

This commit is contained in:
Jörg Breitbart
2019-06-25 16:07:50 +02:00
66 changed files with 4815 additions and 485 deletions
+2 -2
View File
@@ -125,7 +125,7 @@ export class Terminal implements ITerminalApi {
public writeUtf8(data: Uint8Array): void {
this._core.writeUtf8(data);
}
public getOption(key: 'bellSound' | 'bellStyle' | 'cursorStyle' | 'fontFamily' | 'fontWeight' | 'fontWeightBold' | 'rendererType' | 'termName'): string;
public getOption(key: 'bellSound' | 'bellStyle' | 'cursorStyle' | 'fontFamily' | 'fontWeight' | 'fontWeightBold' | 'rendererType' | 'termName' | 'wordSeparator'): string;
public getOption(key: 'allowTransparency' | 'cancelEvents' | 'convertEol' | 'cursorBlink' | 'debug' | 'disableStdin' | 'macOptionIsMeta' | 'rightClickSelectsWord' | 'popOnBell' | 'screenKeys' | 'useFlowControl' | 'visualBell'): boolean;
public getOption(key: 'colors'): string[];
public getOption(key: 'cols' | 'fontSize' | 'letterSpacing' | 'lineHeight' | 'rows' | 'tabStopWidth' | 'scrollback'): number;
@@ -134,7 +134,7 @@ export class Terminal implements ITerminalApi {
public getOption(key: any): any {
return this._core.optionsService.getOption(key);
}
public setOption(key: 'bellSound' | 'fontFamily' | 'termName', value: string): void;
public setOption(key: 'bellSound' | 'fontFamily' | 'termName' | 'wordSeparator', value: string): void;
public setOption(key: 'fontWeight' | 'fontWeightBold', value: 'normal' | 'bold' | '100' | '200' | '300' | '400' | '500' | '600' | '700' | '800' | '900'): void;
public setOption(key: 'bellStyle', value: 'none' | 'visual' | 'sound' | 'both'): void;
public setOption(key: 'cursorStyle', value: 'block' | 'underline' | 'bar'): void;