<!DOCTYPE html>
<html>
  <head>
    <title>Launch Time Benchmark</title>
    <script src="http://code.jquery.com/jquery-1.9.1.min.js"></script>
  </head>
  <body style="font-family: -apple-system; font-size:1.5em;">
    <h2>Benchmark Progress</h2>
    <p id="output" style="white-space: pre-line;"></p>
    <strong id="done"></strong>
  </body>
</html>
<script>
  if (!("WebSocket" in window)) {
    alert("Your browser does not support web sockets");
  } else {
    setup();
  }

  function setup() {
    const host = "ws://localhost:{{ port }}/ws";
    const socket = new WebSocket(host);

    if (socket) {
      socket.onmessage = message => showServerMessage(message.data);
      socket.onclose = () => document.getElementById('done').textContent = 'DONE';
    } else {
      console.log("invalid socket");
    }

    function showServerMessage(text) {
      text = text.replace(/\n/g, "\r\n");
      const output = document.getElementById('output');
      output.textContent = output.textContent.concat(text)
    }
  }
</script>