From f3a916d0af391d9a13cf29d0f43025dcfd8f85ba Mon Sep 17 00:00:00 2001
From: Michal Sojka <michal.sojka@cvut.cz>
Date: Mon, 6 Aug 2018 16:39:28 +0200
Subject: [PATCH] Try to reconnect the disconnected socket every 10 seconds

---
 html/index.html | 58 ++++++++++++++++++++++++++++---------------------
 1 file changed, 33 insertions(+), 25 deletions(-)

diff --git a/html/index.html b/html/index.html
index 51a1455..d244852 100644
--- a/html/index.html
+++ b/html/index.html
@@ -3,38 +3,46 @@
 <title>Merica Terminal</title>
 <script type="text/javascript" src="//dejvice.merica.cz:5000/js" async></script>
 <script>
-    var socket = new WebSocket(
-        "ws://" + document.domain + ':' + location.port,
-        "merica-terminal-protocol"
-    );
+    var socket;
 
-    function updateLocal(msg) {
-        document.getElementById("localJSON").innerHTML = msg;
-    }
+    function connect() {
+        console.log("connecting...");
+	socket = new WebSocket(
+            "ws://" + document.domain + ':' + location.port,
+            "merica-terminal-protocol"
+	);
 
-    socket.onopen = function() {
-        console.log("socket open");
-        updateLocal("socket open");
-    }
+	socket.onopen = function() {
+            console.log("socket open");
+            updateLocal("socket open");
+	}
 
-    socket.onclose = function() {
-        console.log("socket closed");
-        updateLocal("socket closed");
-    }
+	socket.onclose = function() {
+            console.log("socket closed");
+            updateLocal("socket closed");
+	    delete socket;
+	    setTimeout(connect, 10000);
+	}
 
-    socket.onmessage = function(msg) {
-        updateLocal(msg.data);
-        if (typeof updateRemote === "function") {
-            updateRemote(msg.data);
-        } else {
-            if (localStorage) {
-                var now = Date.now();
-                localStorage.setItem(now, msg.data);
-                console.log(now + ": " + msg.data);
+	socket.onmessage = function(msg) {
+            updateLocal(msg.data);
+            if (typeof updateRemote === "function") {
+		updateRemote(msg.data);
+            } else {
+		if (localStorage) {
+                    var now = Date.now();
+                    localStorage.setItem(now, msg.data);
+                    console.log(now + ": " + msg.data);
+		}
             }
-        }
+	}
     }
 
+    connect();
+
+    function updateLocal(msg) {
+        document.getElementById("localJSON").innerHTML = msg;
+    }
     function printLocalStorage() {
         var output = "";
         if (localStorage) {
-- 
2.39.2