Browse Source

Handle disconnect messages from the terminal

Steven Silvester 6 years ago
parent
commit
6b155e6063
1 changed files with 8 additions and 1 deletions
  1. 8 1
      packages/services/src/terminal/default.ts

+ 8 - 1
packages/services/src/terminal/default.ts

@@ -197,6 +197,11 @@ export class DefaultTerminalSession implements TerminalSession.ISession {
 
         const data = JSON.parse(event.data) as JSONPrimitive[];
 
+        // Handle a disconnect message.
+        if (data[0] === 'disconnect') {
+          this._disconnected = true;
+        }
+
         if (this._reconnectAttempt > 0) {
           // After reconnection, ignore all messages until a 'setup' message.
           if (data[0] === 'setup') {
@@ -214,6 +219,7 @@ export class DefaultTerminalSession implements TerminalSession.ISession {
       socket.onopen = (event: MessageEvent) => {
         if (!this._isDisposed) {
           this._isReady = true;
+          this._disconnected = false;
           resolve(undefined);
         }
       };
@@ -232,7 +238,7 @@ export class DefaultTerminalSession implements TerminalSession.ISession {
   }
 
   private _reconnectSocket(): void {
-    if (this._isDisposed || !this._ws) {
+    if (this._isDisposed || !this._ws || this._disconnected) {
       return;
     }
 
@@ -277,6 +283,7 @@ export class DefaultTerminalSession implements TerminalSession.ISession {
   };
   private _reconnectLimit = 7;
   private _reconnectAttempt = 0;
+  private _disconnected = false;
 }
 
 /**