From f0e5866c69ceae633fa21face01ad2b83994cc2b Mon Sep 17 00:00:00 2001
From: murtaugh <murtaugh@xpub.nl>
Date: Thu, 28 May 2020 13:14:50 +0200
Subject: [PATCH] Add '12/shell.html'

---
 12/shell.html | 88 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 88 insertions(+)
 create mode 100644 12/shell.html
diff --git a/12/shell.html b/12/shell.html
new file mode 100644
index 0000000..76e9539
--- /dev/null
+++ b/12/shell.html
@@ -0,0 +1,88 @@
+<!DOCTYPE html>
+<html>
+<head>
+    <meta charset="utf-8">
+    <title>shell</title>
+<style>
+body {
+    background: #888;
+}
+body.connected {
+    background: white;
+}
+#shell {
+    white-space: pre-wrap;
+    height: 25em;
+    width: 100%;
+
+    font-family: monospace;
+    color: white;
+    font-size: 14px;
+    background: black;
+    overflow-y: auto;
+}
+</style>
+</head>
+<body>
+<p><span id="connections">0</span> active connections</p>
+<div id="shell"></div>
+<script>
+var ws_addr = 'wss://'+window.location.host+"/12/pipe/",
+    sock = null,
+    shell = document.getElementById("shell"),
+    connections = document.getElementById("connections");
+
+  function connect () {
+    sock = new WebSocket(ws_addr);
+    sock.onopen = function (event) {
+        console.log("socket opened");
+        document.body.classList.add("connected");
+        // sock.send(JSON.stringify({
+        //     src: "connect",
+        // }));
+    };
+    sock.onmessage = function (event) {
+        // console.log("message", event);
+        if (typeof(event.data) == "string") {
+            var msg = JSON.parse(event.data);
+            // console.log("message JSON", msg);
+            if (msg.src == "stdin" && msg.line) {
+                /*
+		// use a regular expression to parse the line
+		var m = msg.line.match(/^meta:(.*?):(.*)$/);
+		if (m) {
+			// console.log("m", m[1], m[2]);
+			if (m[1] == "title") {
+				shell.innerHTML = m[2];
+			}
+		} else {
+			console.log("bad line", msg.line)
+		}
+		*/
+		
+		// Show all lines
+		var line = document.createElement("div");
+                line.classList.add("line");
+                line.innerHTML = msg.line;
+                shell.appendChild(line);
+		// scroll to bottom
+		shell.scrollTop = shell.scrollHeight;
+            } else if (msg.src == "connect") {
+                connections.innerHTML = msg.connections;
+            }
+        }
+    };
+    sock.onclose = function (event) {
+        // console.log("socket closed");
+        connections.innerHTML = "?";
+        document.body.classList.remove("connected");
+        sock = null;
+        window.setTimeout(connect, 2500);
+    }
+}
+
+connect();
+  
+</script>
+</body>
+</html>
\ No newline at end of file
