equal
deleted
inserted
replaced
1 // svghmi.js |
1 // svghmi.js |
2 |
|
3 var need_cache_apply = []; |
|
4 |
2 |
5 function dispatch_value(index, value) { |
3 function dispatch_value(index, value) { |
6 let widgets = subscribers(index); |
4 let widgets = subscribers(index); |
7 |
5 |
8 let oldval = cache[index]; |
6 let oldval = cache[index]; |
82 |
80 |
83 if(page_fading == "in_progress"){ |
81 if(page_fading == "in_progress"){ |
84 svg_root.classList.remove("fade-out-page"); |
82 svg_root.classList.remove("fade-out-page"); |
85 page_fading = "off"; |
83 page_fading = "off"; |
86 } |
84 } |
87 } |
|
88 |
|
89 while(widget = need_cache_apply.pop()){ |
|
90 widget.apply_cache(); |
|
91 } |
85 } |
92 |
86 |
93 if(jumps_need_update) update_jumps(); |
87 if(jumps_need_update) update_jumps(); |
94 |
88 |
95 |
89 |