|
@@ -205,7 +205,6 @@ class Terminal extends Widget {
|
|
|
if (!this._termOpened) {
|
|
|
this._term.open(this.node);
|
|
|
this._term.element.classList.add(TERMINAL_BODY_CLASS);
|
|
|
- this._setFamily();
|
|
|
this._termOpened = true;
|
|
|
}
|
|
|
|
|
@@ -214,15 +213,6 @@ class Terminal extends Widget {
|
|
|
}
|
|
|
}
|
|
|
|
|
|
- /**
|
|
|
- * A message handler invoked on an `'fit-request'` message.
|
|
|
- */
|
|
|
- protected onFitRequest(msg: Message): void {
|
|
|
- this._setFamily();
|
|
|
- let resize = Widget.ResizeMessage.UnknownSize;
|
|
|
- MessageLoop.sendMessage(this, resize);
|
|
|
- }
|
|
|
-
|
|
|
/**
|
|
|
* Handle `'activate-request'` messages.
|
|
|
*/
|
|
@@ -293,18 +283,6 @@ class Terminal extends Widget {
|
|
|
}
|
|
|
}
|
|
|
|
|
|
- /**
|
|
|
- * Set the font family of the terminal.
|
|
|
- */
|
|
|
- private _setFamily(): void {
|
|
|
- const style = getComputedStyle(document.body);
|
|
|
- const family = style.getPropertyValue('--jp-code-font-family');
|
|
|
- if (family) {
|
|
|
- console.log('setting family', family);
|
|
|
- //this._term.setOption('fontFamily', '"Source Code Pro", monospace');
|
|
|
- }
|
|
|
- }
|
|
|
-
|
|
|
private _term: Xterm;
|
|
|
private _needsResize = true;
|
|
|
private _theme: Terminal.Theme = 'dark';
|