summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/public/repl.js
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud@pankzsoft.com>2025-11-05 14:23:03 +0100
committerArnaud Bailly <arnaud@pankzsoft.com>2025-11-05 14:23:03 +0100
commitafcfa146122179dc80dd8055314b1381d152fb09 (patch)
tree2aa2d930f89fa308d016c92c43395edaacbfcb99 /lambda-calcul/haskell/public/repl.js
parent71fa7dfdc873b014bf1b5b8ea648e803bff67724 (diff)
downloadlambda-nantes-afcfa146122179dc80dd8055314b1381d152fb09.tar.gz
provide session id to user so they can reconnect
Diffstat (limited to 'lambda-calcul/haskell/public/repl.js')
-rw-r--r--lambda-calcul/haskell/public/repl.js6
1 files changed, 4 insertions, 2 deletions
diff --git a/lambda-calcul/haskell/public/repl.js b/lambda-calcul/haskell/public/repl.js
index 22068f1..8f5d619 100644
--- a/lambda-calcul/haskell/public/repl.js
+++ b/lambda-calcul/haskell/public/repl.js
@@ -7,7 +7,7 @@ function generateRandomToken() {
}
function connect() {
- websocket = (function() {
+ [websocket, token] = (function() {
const host = window.location.host;
const params = new URLSearchParams(window.location.search);
let token = generateRandomToken();
@@ -17,7 +17,7 @@ function connect() {
const protocol = window.location.protocol === "https:" ? "wss:" : "ws:";
const ws = new WebSocket(protocol + "//" + host + "/repl/" + token);
ws.binaryType = "arraybuffer";
- return ws;
+ return [ws, token];
})();
websocket.onopen = function(e) {
@@ -25,6 +25,7 @@ function connect() {
document.getElementById("command").classList.add("connected");
document.getElementById("connect").src = "images/connected.png";
document.getElementById("connect").removeEventListener("click", connect);
+ document.getElementById("session").appendChild(document.createTextNode("Session: " + token));
};
websocket.onclose = function(e) {
@@ -32,6 +33,7 @@ function connect() {
document.getElementById("command").classList.add("disconnected");
document.getElementById("connect").src = "images/connect.png";
document.getElementById("connect").addEventListener("click", connect);
+ document.getElementById("session").children.each((node) => node.remove());
};
websocket.onmessage = function(e) {