svghmi/svghmi.js
changeset 3680 20f9f0c36ad6
parent 3664 7e8db0b44e42
child 3683 bbcbb1bba9f1
equal deleted inserted replaced
3664:7e8db0b44e42 3680:20f9f0c36ad6
   635 function ws_onclose(evt) {
   635 function ws_onclose(evt) {
   636     console.log("Connection closed. code:"+evt.code+" reason:"+evt.reason+" wasClean:"+evt.wasClean+" Reload in "+reconnect_delay+"ms.");
   636     console.log("Connection closed. code:"+evt.code+" reason:"+evt.reason+" wasClean:"+evt.wasClean+" Reload in "+reconnect_delay+"ms.");
   637     ws = null;
   637     ws = null;
   638     // reconect
   638     // reconect
   639     // TODO : add visible notification while waiting for reload
   639     // TODO : add visible notification while waiting for reload
       
   640     console.log(evt.wasClean)
       
   641     console.log(evt.reason)
       
   642     if(evt.code=1000){
       
   643         // Do not attempt to reconnect immediately in case of Normal Closure
       
   644         window.alert("Connection closed by server");
       
   645         location.reload();
       
   646     }
   640     window.setTimeout(create_ws, reconnect_delay);
   647     window.setTimeout(create_ws, reconnect_delay);
   641     reconnect_delay += 500;
   648     reconnect_delay += 500;
   642 };
   649 };
   643 
   650 
   644 var ws_url =
   651 var ws_url =