64 )), size + 1]; /* total increment */ |
64 )), size + 1]; /* total increment */ |
65 } |
65 } |
66 }; |
66 }; |
67 |
67 |
68 // Apply updates recieved through ws.onmessage to subscribed widgets |
68 // Apply updates recieved through ws.onmessage to subscribed widgets |
69 // Do the page swith if any one pending |
69 function apply_updates() { |
70 // Called on requestAnimationFrame, modifies DOM |
|
71 function animate() { |
|
72 if(current_subscribed_page != current_visible_page){ |
|
73 switch_visible_page(current_subscribed_page); |
|
74 } |
|
75 |
|
76 for(let index in updates){ |
70 for(let index in updates){ |
77 // serving as a key, index becomes a string |
71 // serving as a key, index becomes a string |
78 // -> pass Number(index) instead |
72 // -> pass Number(index) instead |
79 dispatch_value(Number(index), updates[index]); |
73 dispatch_value(Number(index), updates[index]); |
80 delete updates[index]; |
74 delete updates[index]; |
81 } |
75 } |
|
76 } |
|
77 |
|
78 // Called on requestAnimationFrame, modifies DOM |
|
79 var requestAnimationFrameID = null; |
|
80 function animate() { |
|
81 // Do the page swith if any one pending |
|
82 if(current_subscribed_page != current_visible_page){ |
|
83 switch_visible_page(current_subscribed_page); |
|
84 } |
|
85 console.log("no page switch"); |
|
86 apply_updates(); |
82 requestAnimationFrameID = null; |
87 requestAnimationFrameID = null; |
83 } |
88 } |
84 |
89 |
85 var requestAnimationFrameID = null; |
|
86 function requestHMIAnimation() { |
90 function requestHMIAnimation() { |
87 if(requestAnimationFrameID == null){ |
91 if(requestAnimationFrameID == null){ |
88 requestAnimationFrameID = window.requestAnimationFrame(animate); |
92 requestAnimationFrameID = window.requestAnimationFrame(animate); |
89 } |
93 } |
90 } |
94 } |