websocket.html 2.0 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990
  1. <html>
  2. <head>
  3. <style>
  4. #rx {
  5. font-family: 'Courier New', Courier, monospace;
  6. font-size: small;
  7. }
  8. </style>
  9. <script type="text/javascript" src="common.js?v=$COMMIT_HASH"></script>
  10. </head>
  11. <body>
  12. <div id="state">State: Please wait...</div>
  13. <hr>
  14. <div id="img">Image: Please wait...</div>
  15. <hr>
  16. <div id="rx">Events:<br></div>
  17. <script>
  18. var gateway = getDomainname().replace("http://", "ws://") + "/ws";
  19. var websocket;
  20. window.addEventListener('load', onLoad);
  21. function initWebSocket() {
  22. console.log('Trying to open a WebSocket connection...');
  23. addToLog('Trying to open a WebSocket connection...');
  24. websocket = new WebSocket(gateway);
  25. websocket.onopen = onOpen;
  26. websocket.onclose = onClose;
  27. websocket.onmessage = onMessage; // <-- add this line
  28. }
  29. function onOpen(event) {
  30. console.log('Connection opened');
  31. addToLog('Connection opened');
  32. }
  33. function onClose(event) {
  34. console.log('Connection closed');
  35. addToLog('Connection closed');
  36. setTimeout(initWebSocket, 2000);
  37. }
  38. function onMessage(event) {
  39. console.log(event);
  40. addToLog(event.data);
  41. data = JSON.parse(event.data)
  42. // State
  43. if (data.hasOwnProperty("state")) {
  44. processStateChange(data.state);
  45. }
  46. }
  47. function onLoad(event) {
  48. initWebSocket();
  49. }
  50. function addToLog(msg) {
  51. document.getElementById('rx').innerHTML += "[" + new Date().toLocaleTimeString() + "] " + msg + "<br>\n";
  52. window.scrollBy(0,document.body.scrollHeight);
  53. }
  54. function processStateChange(state) {
  55. document.getElementById('state').innerHTML = "State: <b>" + data.state + "</b>";
  56. // TODO only reload image for those steps where it changed...
  57. var d = new Date();
  58. var timestamp = d.getTime();
  59. document.getElementById('img').innerHTML = 'Image: <br><img src=' + getDomainname() + '/img_tmp/alg_roi.jpg?timestamp='+ timestamp +'" height=200px;"></img>';
  60. }
  61. function updateImage() {
  62. }
  63. </script>
  64. </body>
  65. </html>