From 490b8fd3ef72ac9e053ed6afc1776b2a28308c74 Mon Sep 17 00:00:00 2001 From: Min RK Date: Sat, 2 Mar 2019 12:19:03 +0100 Subject: [PATCH] trigger _ws_closed on any close event MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit it doesn’t matter if the close was clean or not, we should still handle the close event. we set a different onclose handler prior to the client requesting close, which is likely what the old wasClean checks were for --- notebook/static/services/kernels/kernel.js | 32 ++++++++++------------ 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/notebook/static/services/kernels/kernel.js b/notebook/static/services/kernels/kernel.js index 50555394d..841450457 100644 --- a/notebook/static/services/kernels/kernel.js +++ b/notebook/static/services/kernels/kernel.js @@ -470,33 +470,31 @@ define([ var already_called_onclose = false; // only alert once var ws_closed_early = function(evt){ + console.log("WebSocket closed early", evt); if (already_called_onclose){ return; } already_called_onclose = true; - if ( ! evt.wasClean ){ - // If the websocket was closed early, that could mean - // that the kernel is actually dead. Try getting - // information about the kernel from the API call -- - // if that fails, then assume the kernel is dead, - // otherwise just follow the typical websocket closed - // protocol. - that.get_info(function () { - that._ws_closed(ws_host_url, false); - }, function () { - that.events.trigger('kernel_dead.Kernel', {kernel: that}); - that._kernel_dead(); - }); - } + // If the websocket was closed early, that could mean + // that the kernel is actually dead. Try getting + // information about the kernel from the API call -- + // if that fails, then assume the kernel is dead, + // otherwise just follow the typical websocket closed + // protocol. + that.get_info(function () { + that._ws_closed(ws_host_url, false); + }, function () { + that.events.trigger('kernel_dead.Kernel', {kernel: that}); + that._kernel_dead(); + }); }; var ws_closed_late = function(evt){ + console.log("WebSocket closed unexpectedly", evt); if (already_called_onclose){ return; } already_called_onclose = true; - if ( ! evt.wasClean ){ - that._ws_closed(ws_host_url, false); - } + that._ws_closed(ws_host_url, false); }; var ws_error = function(evt){ if (already_called_onclose){