--- a/svghmi/svghmi.js Fri Mar 06 09:35:08 2020 +0100
+++ b/svghmi/svghmi.js Fri Mar 06 14:42:08 2020 +0100
@@ -2,6 +2,7 @@
var cache = hmitree_types.map(_ignored => undefined);
function dispatch_value_to_widget(widget, index, value, oldval) {
@@ -66,8 +67,14 @@
// Apply updates recieved through ws.onmessage to subscribed widgets
+// Do the page swith if any one pending // Called on requestAnimationFrame, modifies DOM
-function apply_pending_updates() {
+ if(page_switch != null){ + do_switch_page(page_switch); for(let index in updates){
// serving as a key, index becomes a string
// -> pass Number(index) instead
@@ -76,6 +83,15 @@
+var requestAnimationFrameID = null; +function requestHMIAnimation() { + if(requestAnimationFrameID != null){ + window.cancelAnimationFrame(requestAnimationFrameID); + requestAnimationFrameID = null; + requestAnimationFrameID = window.requestAnimationFrame(animate); // Message reception handler
// Hash is verified and HMI values updates resulting from binary parsing
// are stored until browser can compute next frame, DOM is left untouched
@@ -106,7 +122,7 @@
// register for rendering on next frame, since there are updates
- window.requestAnimationFrame(apply_pending_updates);
+ window.requestAnimationFrame(animate); // 1003 is for "Unsupported Data"
// ws.close(1003, err.message);
@@ -241,6 +257,11 @@
function switch_page(page_name) {
+ page_switch = page_name; + window.requestAnimationFrame(animate); +function do_switch_page(page_name) { let old_desc = page_desc[current_page];
let new_desc = page_desc[page_name];
@@ -289,7 +310,7 @@
svg_root.setAttribute('viewBox',new_desc.bbox.join(" "));
current_page = page_name;
- update_subscriptions();
+ window.setTimeout(update_subscriptions,0);