Add '12/shell.html'

5 years ago · f0e5866c69
parent a18d779bda
commit f0e5866c69
1 changed files with 88 additions and 0 deletions
--- a/12/shell.html
+++ 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>