Browse Source

Merge pull request #149 from blink1073/before-detach

Ask whether to shut down the kernel when detaching from the DOM
Min RK 9 years ago
parent
commit
2da5d98565
1 changed files with 12 additions and 0 deletions
  1. 12 0
      src/notebook/notebook/widget.ts

+ 12 - 0
src/notebook/notebook/widget.ts

@@ -376,6 +376,18 @@ class NotebookWidget extends Widget {
     this.node.removeEventListener('dblclick', this);
     this.node.removeEventListener('focus', this, true);
     this.node.removeEventListener('blur', this, true);
+    let session = this.model.session;
+    if (session && session.status !== KernelStatus.Dead) {
+      showDialog({
+        title: 'Shutdown kernel?',
+        body: `Shutdown "${session.kernel.name}" kernel?`,
+        host: this.node
+      }).then(result => {
+        if (result.text === 'OK') {
+          session.shutdown();
+        }
+      });
+    }
   }
 
   /**