Kaynağa Gözat

Terminal refresh bugfix (#3374)

* Clean up.

* Fixes https://github.com/jupyterlab/jupyterlab/issues/3181

* Fix docs
Afshin Darian 7 yıl önce
ebeveyn
işleme
f525c3e8ea

+ 2 - 2
docs/notebook.md

@@ -86,8 +86,8 @@ A [CodeCell](http://jupyterlab.github.io/jupyterlab/classes/_cells_src_widget_.c
 also contains an [OutputArea](http://jupyterlab.github.io/jupyterlab/classes/_outputarea_src_widget_.outputarea.html).
 An OutputArea is responsible for rendering the outputs in the
 [OutputAreaModel](http://jupyterlab.github.io/jupyterlab/classes/_outputarea_src_model_.outputareamodel.html)
-list. An OutputArea uses a
-notebook-specific [RenderMimeRegistry](http://jupyterlab.github.io/jupyterlab/classes/_rendermime_src_registry_.rendermimeregistry.html)
+list. An OutputArea uses a notebook-specific
+[RenderMimeRegistry](http://jupyterlab.github.io/jupyterlab/classes/_rendermime_src_registry_.rendermimeregistry.html)
 object to render `display_data` output messages.
 
 #### Rendering output messages

+ 5 - 7
packages/apputils/src/thememanager.ts

@@ -123,17 +123,15 @@ class ThemeManager {
   loadCSS(path: string): Promise<void> {
     const link = document.createElement('link');
     const delegate = new PromiseDelegate<void>();
-    let href = URLExt.join(this._baseUrl, path);
-
-    if (!URLExt.isLocal(path)) {
-      href = path;
-    }
+    const href = URLExt.isLocal(path) ? URLExt.join(this._baseUrl, path) : path;
 
     link.rel = 'stylesheet';
     link.type = 'text/css';
     link.href = href;
-    link.onload = () => { delegate.resolve(void 0); };
-    link.onerror = () => { delegate.reject(`Stylesheet failed to load: ${href}`); };
+    link.addEventListener('load', () => { delegate.resolve(undefined); });
+    link.addEventListener('error', () => {
+      delegate.reject(`Stylesheet failed to load: ${href}`);
+    });
     document.body.appendChild(link);
     this._links.push(link);
 

+ 47 - 33
packages/services/src/terminal/default.ts

@@ -106,6 +106,7 @@ class DefaultTerminalSession implements TerminalSession.ISession {
     if (this._isDisposed) {
       return;
     }
+
     this._isDisposed = true;
     if (this._ws) {
       this._ws.close();
@@ -123,16 +124,20 @@ class DefaultTerminalSession implements TerminalSession.ISession {
       return;
     }
 
-    let msg: JSONPrimitive[] = [message.type];
-    msg.push(...message.content);
-    let value = JSON.stringify(msg);
-    if (this._isReady && this._ws) {
-      this._ws.send(value);
+    const msg = [message.type, ...message.content];
+    const socket = this._ws;
+    const value = JSON.stringify(msg);
+
+    if (this._isReady && socket) {
+      socket.send(value);
       return;
     }
+
     this.ready.then(() => {
-      if (this._ws) {
-        this._ws.send(value);
+      const socket = this._ws;
+
+      if (socket) {
+        socket.send(value);
       }
     });
   }
@@ -151,43 +156,50 @@ class DefaultTerminalSession implements TerminalSession.ISession {
    * Shut down the terminal session.
    */
   shutdown(): Promise<void> {
-    return DefaultTerminalSession.shutdown(this.name, this.serverSettings);
+    const { name, serverSettings } = this;
+    return DefaultTerminalSession.shutdown(name, serverSettings);
   }
 
   /**
    * Clone the current session object.
    */
   clone(): TerminalSession.ISession {
-    return new DefaultTerminalSession(this.name, {
-      serverSettings: this.serverSettings
-    });
+    const { name, serverSettings } = this;
+    return new DefaultTerminalSession(name, { serverSettings });
   }
 
   /**
    * Connect to the websocket.
    */
   private _initializeSocket(): Promise<void> {
-    let name = this._name;
-    if (this._ws) {
-      this._ws.close();
+    const name = this._name;
+    let socket = this._ws;
+
+    if (socket) {
+      socket.close();
     }
     this._isReady = false;
-    let settings = this.serverSettings;
+
+    const settings = this.serverSettings;
+    const token = this.serverSettings.token;
+
     this._url = Private.getTermUrl(settings.baseUrl, this._name);
     Private.running[this._url] = this;
+
     let wsUrl = URLExt.join(settings.wsUrl, `terminals/websocket/${name}`);
-    let token = this.serverSettings.token;
+
     if (token) {
       wsUrl = wsUrl + `?token=${token}`;
     }
-    this._ws = new settings.WebSocket(wsUrl);
+    socket = this._ws = new settings.WebSocket(wsUrl);
 
-    this._ws.onmessage = (event: MessageEvent) => {
+    socket.onmessage = (event: MessageEvent) => {
       if (this._isDisposed) {
         return;
       }
 
-      let data = JSON.parse(event.data) as JSONPrimitive[];
+      const data = JSON.parse(event.data) as JSONPrimitive[];
+
       this._messageReceived.emit({
         type: data[0] as TerminalSession.MessageType,
         content: data.slice(1)
@@ -195,32 +207,34 @@ class DefaultTerminalSession implements TerminalSession.ISession {
     };
 
     return new Promise<void>((resolve, reject) => {
-      if (!this._ws) {
+      const socket = this._ws;
+
+      if (!socket) {
         return;
       }
-      this._ws.onopen = (event: MessageEvent) => {
-        if (this._isDisposed) {
-          return;
+
+      socket.onopen = (event: MessageEvent) => {
+        if (!this._isDisposed) {
+          this._isReady = true;
+          resolve(undefined);
         }
-        this._isReady = true;
-        resolve(void 0);
       };
-      this._ws.onerror = (event: Event) => {
-        if (this._isDisposed) {
-          return;
+
+      socket.onerror = (event: Event) => {
+        if (!this._isDisposed) {
+          reject(event);
         }
-        reject(event);
       };
     });
   }
 
-  private _name: string;
-  private _url: string;
-  private _ws: WebSocket | null = null;
   private _isDisposed = false;
-  private _readyPromise: Promise<void>;
   private _isReady = false;
   private _messageReceived = new Signal<this, TerminalSession.IMessage>(this);
+  private _name: string;
+  private _readyPromise: Promise<void>;
+  private _url: string;
+  private _ws: WebSocket | null = null;
 }
 
 

+ 11 - 17
packages/terminal-extension/src/index.ts

@@ -22,7 +22,7 @@ import {
 } from '@jupyterlab/services';
 
 import {
-  Terminal, ITerminalTracker
+  ITerminalTracker, Terminal
 } from '@jupyterlab/terminal';
 
 
@@ -63,9 +63,7 @@ const plugin: JupyterLabPlugin<ITerminalTracker> = {
   activate,
   id: '@jupyterlab/terminal-extension:plugin',
   provides: ITerminalTracker,
-  requires: [
-    IMainMenu, ICommandPalette, ILayoutRestorer
-  ],
+  requires: [IMainMenu, ICommandPalette, ILayoutRestorer],
   optional: [ILauncher],
   autoStart: true
 };
@@ -116,9 +114,7 @@ function activate(app: JupyterLab, mainMenu: IMainMenu, palette: ICommandPalette
     CommandIDs.increaseFont,
     CommandIDs.decreaseFont,
     CommandIDs.toggleTheme
-  ].forEach(command => {
-    palette.addItem({ command, category });
-  });
+  ].forEach(command => { palette.addItem({ command, category }); });
 
   // Add terminal creation to the file menu.
   mainMenu.fileMenu.newMenu.addItem({ command: CommandIDs.createNew });
@@ -130,9 +126,7 @@ function activate(app: JupyterLab, mainMenu: IMainMenu, palette: ICommandPalette
       category: 'Other',
       rank: 0,
       iconClass: TERMINAL_ICON_CLASS,
-      callback: () => {
-        return commands.execute(CommandIDs.createNew);
-      }
+      callback: () => commands.execute(CommandIDs.createNew)
     });
   }
 
@@ -162,22 +156,22 @@ function addCommands(app: JupyterLab, services: ServiceManager, tracker: Instanc
     label: 'Terminal',
     caption: 'Start a new terminal session',
     execute: args => {
-      let name = args['name'] as string;
-      let initialCommand = args['initialCommand'] as string;
-      let term = new Terminal({ initialCommand });
+      const name = args['name'] as string;
+      const initialCommand = args['initialCommand'] as string;
+      const term = new Terminal({ initialCommand });
+      const promise = name ? services.terminals.connectTo(name)
+        : services.terminals.startNew();
+
       term.title.closable = true;
       term.title.icon = TERMINAL_ICON_CLASS;
       term.title.label = '...';
       shell.addToMainArea(term);
 
-      let promise = name ?
-        services.terminals.connectTo(name)
-        : services.terminals.startNew();
-
       return promise.then(session => {
         term.session = session;
         tracker.add(term);
         shell.activateById(term.id);
+
         return term;
       }).catch(() => { term.dispose(); });
     }

+ 20 - 26
packages/terminal/src/widget.ts

@@ -125,7 +125,7 @@ class Terminal extends Widget {
       return;
     }
     this._fontSize = size;
-    this._needsSnap = true;
+    this._needsResize = true;
     this.update();
   }
 
@@ -224,10 +224,9 @@ class Terminal extends Widget {
     if (!this.isVisible) {
       return;
     }
-    if (this._needsSnap) {
-      this._snapTermSizing();
-    }
+
     if (this._needsResize) {
+      this._snapTermSizing();
       this._resizeTerminal();
     }
   }
@@ -290,33 +289,30 @@ class Terminal extends Widget {
    * Use the dummy terminal to measure the row and column sizes.
    */
   private _snapTermSizing(): void {
+    const node = this._dummyTerm;
+
     this._term.element.style.fontSize = `${this.fontSize}px`;
-    let node = this._dummyTerm;
     this._term.element.appendChild(node);
     this._rowHeight = node.offsetHeight / DUMMY_ROWS;
     this._colWidth = node.offsetWidth / DUMMY_COLS;
     this._term.element.removeChild(node);
-    this._needsSnap = false;
-    this._needsResize = true;
   }
 
   /**
    * Resize the terminal based on computed geometry.
    */
   private _resizeTerminal() {
-    let offsetWidth = this._offsetWidth;
-    let offsetHeight = this._offsetHeight;
-    if (offsetWidth < 0) {
-      offsetWidth = this.node.offsetWidth;
-    }
-    if (offsetHeight < 0) {
-      offsetHeight = this.node.offsetHeight;
-    }
-    let box = this._box || (this._box = ElementExt.boxSizing(this.node));
-    let height = offsetHeight - box.verticalSum;
-    let width = offsetWidth - box.horizontalSum;
-    let rows = Math.floor(height / this._rowHeight) - 1;
-    let cols = Math.floor(width / this._colWidth) - 1;
+    const { node } = this;
+    const offsetWidth = this._offsetWidth < 0 ? node.offsetWidth
+      : this._offsetWidth;
+    const offsetHeight = this._offsetHeight < 0 ? node.offsetHeight
+      : this._offsetHeight;
+    const box = this._box = ElementExt.boxSizing(this.node);
+    const height = offsetHeight - box.verticalSum;
+    const width = offsetWidth - box.horizontalSum;
+    const rows = Math.floor(height / this._rowHeight) - 1;
+    const cols = Math.floor(width / this._colWidth) - 1;
+
     this._term.resize(cols, rows);
     this._sessionSize = [rows, cols, height, width];
     this._setSessionSize();
@@ -327,18 +323,16 @@ class Terminal extends Widget {
    * Send the size to the session.
    */
   private _setSessionSize(): void {
-    if (this._session) {
-      this._session.send({
-        type: 'set_size',
-        content: this._sessionSize
-      });
+    const session = this._session;
+
+    if (session) {
+      session.send({ type: 'set_size', content: this._sessionSize });
     }
   }
 
   private _term: Xterm;
   private _dummyTerm: HTMLElement;
   private _fontSize = -1;
-  private _needsSnap = true;
   private _needsResize = true;
   private _rowHeight = -1;
   private _colWidth = -1;