core: Ignore websocket errors when navigating away from the page (ie, Abnormal closure when switching apps). #60
All checks were successful
Build Tilde Friends / Build-All (push) Successful in 32m21s
All checks were successful
Build Tilde Friends / Build-All (push) Successful in 32m21s
This commit is contained in:
@ -8,6 +8,7 @@ let gFiles = {};
|
|||||||
let gApp = {files: {}, emoji: '📦'};
|
let gApp = {files: {}, emoji: '📦'};
|
||||||
let gEditor;
|
let gEditor;
|
||||||
let gOriginalInput;
|
let gOriginalInput;
|
||||||
|
let gUnloading;
|
||||||
|
|
||||||
let kErrorColor = '#dc322f';
|
let kErrorColor = '#dc322f';
|
||||||
let kDisconnectColor = '#f00';
|
let kDisconnectColor = '#f00';
|
||||||
@ -1560,6 +1561,9 @@ function connectSocket(path) {
|
|||||||
_receive_websocket_message(JSON.parse(event.data));
|
_receive_websocket_message(JSON.parse(event.data));
|
||||||
};
|
};
|
||||||
gSocket.onclose = function (event) {
|
gSocket.onclose = function (event) {
|
||||||
|
if (gUnloading) {
|
||||||
|
setStatusMessage('⚪ Closing...', kStatusColor);
|
||||||
|
} else {
|
||||||
const k_codes = {
|
const k_codes = {
|
||||||
1000: 'Normal closure',
|
1000: 'Normal closure',
|
||||||
1001: 'Going away',
|
1001: 'Going away',
|
||||||
@ -1581,6 +1585,7 @@ function connectSocket(path) {
|
|||||||
'🔴 Closed: ' + (k_codes[event.code] || event.code),
|
'🔴 Closed: ' + (k_codes[event.code] || event.code),
|
||||||
kDisconnectColor
|
kDisconnectColor
|
||||||
);
|
);
|
||||||
|
}
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -1854,6 +1859,9 @@ window.addEventListener('load', function () {
|
|||||||
window.addEventListener('blur', blur);
|
window.addEventListener('blur', blur);
|
||||||
window.addEventListener('message', message, false);
|
window.addEventListener('message', message, false);
|
||||||
window.addEventListener('online', connectSocket);
|
window.addEventListener('online', connectSocket);
|
||||||
|
window.addEventListener('beforeunload', function () {
|
||||||
|
gUnloading = true;
|
||||||
|
});
|
||||||
document.getElementById('name').value = window.location.pathname;
|
document.getElementById('name').value = window.location.pathname;
|
||||||
document
|
document
|
||||||
.getElementById('closeEditor')
|
.getElementById('closeEditor')
|
||||||
|
Reference in New Issue
Block a user