+
+let websocket = null;
+
+function open_ws()
+{
+ console.log("Connecting...");
+ try {
+ if (websocket)
+ websocket.close();
+ websocket = new WebSocket("ws://127.0.0.1:5250/");
+ websocket.onopen = function(evt) {
+ console.log("Connected to client.");
+ };
+ websocket.onclose = function(evt) {
+ console.log("Disconnected from client.");
+ setTimeout(open_ws, 100);
+ };
+ websocket.onmessage = function(evt) {
+ let msg = evt.data;
+ let m = msg.match(/^update (.*)/);
+ if (m !== null) {
+ update(m[1]);
+ }
+ m = msg.match(/^eval (.*)/);
+ if (m !== null) {
+ eval(m[1]);
+ }
+ };
+ websocket.onerror = function(evt) {
+ console.log('Error: ' + evt.data);
+ };
+ } catch (exception) {
+ console.log('Error: ' + exception);
+ setTimeout(open_ws, 100);
+ }
+};
+open_ws();