1 // svghmi.js

     1 // svghmi.js

     2 

     2 

     3 var cache = hmitree_types.map(_ignored => undefined);

     3 var cache = hmitree_types.map(_ignored => undefined);

     4 var updates = {};

     4 var updates = {};

     5 var need_cache_apply = []; 

     5 var need_cache_apply = []; 

     6 

     7 

     7 function dispatch_value_to_widget(widget, index, value, oldval) {

     8 function dispatch_value_to_widget(widget, index, value, oldval) {

     8     try {

     9     try {

     9         let idx = widget.offset ? index - widget.offset : index;

    10         let idx = widget.offset ? index - widget.offset : index;

    10         let idxidx = widget.indexes.indexOf(idx);

    11         let idxidx = widget.indexes.indexOf(idx);

   269 

   270 

   270 function switch_page(page_name, page_index) {

   271 function switch_page(page_name, page_index) {

   271     if(current_subscribed_page != current_visible_page){

   272     if(current_subscribed_page != current_visible_page){

   272         /* page switch already going */

   273         /* page switch already going */

   273         /* TODO LOG ERROR */

   274         /* TODO LOG ERROR */

   275     }

   276     }

   276 

   277 

   277     if(page_name == undefined)

   278     if(page_name == undefined)

   278         page_name = current_subscribed_page;

   279         page_name = current_subscribed_page;

   279 

   280 

   281 };

   282 };

   282 

   283 

   283 function* chain(a,b){

   284 function* chain(a,b){

   284     yield* a;

   285     yield* a;

   285     yield* b;

   286     yield* b;

   371     let old_desc = page_desc[current_subscribed_page];

   372     let old_desc = page_desc[current_subscribed_page];

   372     let new_desc = page_desc[page_name];

   373     let new_desc = page_desc[page_name];

   373 

   374 

   374     if(new_desc == undefined){

   375     if(new_desc == undefined){

   375         /* TODO LOG ERROR */

   376         /* TODO LOG ERROR */

   377     }

   378     }

   378 

   379 

   379     if(page_index == undefined){

   380     if(page_index == undefined){

   380         page_index = new_desc.page_index;

   381         page_index = new_desc.page_index;

   381     }

   382     }

   391     update_subscriptions();

   392     update_subscriptions();

   392 

   393 

   393     current_subscribed_page = page_name;

   394     current_subscribed_page = page_name;

   394 

   395 

   395     requestHMIAnimation();

   396     requestHMIAnimation();

   396 }

   401 }

   397 

   402 

   398 function switch_visible_page(page_name) {

   403 function switch_visible_page(page_name) {

   399 

   404 

   400     let old_desc = page_desc[current_visible_page];

   405     let old_desc = page_desc[current_visible_page];