فهرست منبع

Design updates to terminal

* White on black
* 14px font size
* monospace font
* Set defaults in widget, don't override in plugin
Brian E. Granger 8 سال پیش
والد
کامیت
33e24b728c
3فایلهای تغییر یافته به همراه6 افزوده شده و 5 حذف شده
  1. 3 3
      src/terminal/index.ts
  2. 0 2
      src/terminal/plugin.ts
  3. 3 0
      src/terminal/theme.css

+ 3 - 3
src/terminal/index.ts

@@ -319,9 +319,9 @@ class TerminalWidget extends Widget {
     this._term.open(this.node);
     this._term.element.classList.add(TERMINAL_BODY_CLASS);
 
-    this.fontSize = options.fontSize || 11;
-    this.background = options.background || 'white';
-    this.color = options.color || 'black';
+    this.fontSize = options.fontSize || 14;
+    this.background = options.background || 'black';
+    this.color = options.color || 'white';
 
     this._term.on('data', (data: string) => {
       this._ws.send(JSON.stringify(['stdin', data]));

+ 0 - 2
src/terminal/plugin.ts

@@ -32,8 +32,6 @@ function activateTerminal(app: Application): Promise<void> {
     id: newTerminalId,
     handler: () => {
       let term = new TerminalWidget();
-      term.color = 'black';
-      term.background = 'white';
       term.title.closable = true;
       app.shell.addToMainArea(term);
       let stack = term.parent;

+ 3 - 0
src/terminal/theme.css

@@ -18,3 +18,6 @@
 
 @import '~xterm/src/xterm.css';
 
+.terminal {
+  font-family: monospace;
+}