svghmi/svghmi.js
branchsvghmi
changeset 3005 ff9ae4f4e3be
parent 3000 a9a45977bac0
child 3006 bbffdefd2eed
equal deleted inserted replaced
3004:705e34c6fe93 3005:ff9ae4f4e3be
   321     if(page_index == undefined){
   321     if(page_index == undefined){
   322         page_index = new_desc.page_index;
   322         page_index = new_desc.page_index;
   323     }
   323     }
   324 
   324 
   325     if(old_desc){
   325     if(old_desc){
   326         old_desc.absolute_widgets.map(w=>w.unsub());
   326         old_desc.widgets.map(([widget,relativeness])=>widget.unsub());
   327         old_desc.relative_widgets.map(w=>w.unsub());
   327     }
   328     }
       
   329     new_desc.absolute_widgets.map(w=>w.sub());
       
   330     var new_offset = page_index == undefined ? 0 : page_index - new_desc.page_index;
   328     var new_offset = page_index == undefined ? 0 : page_index - new_desc.page_index;
   331     new_desc.relative_widgets.map(w=>w.sub(new_offset));
   329     new_desc.widgets.map(([widget,relativeness])=>widget.sub(new_offset,relativeness));
   332 
   330 
   333     update_subscriptions();
   331     update_subscriptions();
   334 
   332 
   335     current_subscribed_page = page_name;
   333     current_subscribed_page = page_name;
   336     current_page_index = page_index;
   334     current_page_index = page_index;