function "jump_widget_activity" {
optional_labels("active inactive");
function "jump_widget_disability" {
optional_labels("disabled");
template "widget[@type='Jump']", mode="widget_defs" {
const "activity" call "jump_widget_activity" with "hmi_element", "$hmi_element";
const "have_activity","string-length($activity)>0";
const "disability" call "jump_widget_disability" with "hmi_element", "$hmi_element";
const "have_disability","$have_activity and string-length($disability)>0";
| dispatch: function(value) {
| this.disabled = !Number(value);
| this.disabled_elt.setAttribute("style", this.active_elt_style);
| this.inactive_elt.setAttribute("style", "display:none");
| this.active_elt.setAttribute("style", "display:none");
| this.disabled_elt.setAttribute("style", "display:none");
| this.active_elt.setAttribute("style", this.active_elt_style);
| this.inactive_elt.setAttribute("style", "display:none");
| this.inactive_elt.setAttribute("style", this.inactive_elt_style);
| this.active_elt.setAttribute("style", "display:none");
| on_click: function(evt) {
| const index = this.indexes.length > 0 ? this.indexes[0] + this.offset : undefined;
| const name = this.args[0];
| switch_page(name, index);
| notify_page_change: function(page_name, index){
| const ref_index = this.indexes.length > 0 ? this.indexes[0] + this.offset : undefined;
| const ref_name = this.args[0];
| this.active =((ref_name == undefined || ref_name == page_name) && index == ref_index);
/* registering event this way does not "click" through svg:use
| this.element.onclick = evt => switch_page(this.args[0]);
event must be registered by adding attribute to element instead
TODO : generalize mouse event handling by global event capture + getElementsAtPoint()
| this.element.setAttribute("onclick", "hmi_widgets['«$hmi_element/@id»'].on_click(evt)");
| this.active_elt_style = this.active_elt.getAttribute("style");
| this.inactive_elt_style = this.inactive_elt.getAttribute("style");
when "$have_disability" {
| this.disabled_elt_style = this.disabled_elt.getAttribute("style");
| this.unsubscribable = true;
template "widget[@type='Jump']", mode="per_page_widget_template"{
/* check that given path is compatible with page's reference path */
/* when no page name provided, check for same page */
const "target_page_name" choose {
when "arg" value "arg[1]/@value";
otherwise value "$page_desc/arg[1]/@value";
const "target_page_path" choose {
when "arg" value "$hmi_pages_descs[arg[1]/@value = $target_page_name]/path[1]/@value";
otherwise value "$page_desc/path[1]/@value";
if "not(func:same_class_paths($target_page_path, path[1]/@value))"
error > Jump id="«@id»" to page "«$target_page_name»" with incompatible path "«path[1]/@value» (must be same class as "«$target_page_path»")
var jumps_need_update = false;
var jump_history = [[default_page, undefined]];
function update_jumps() {
page_desc[current_visible_page].jumps.map(w=>w.notify_page_change(current_visible_page,current_page_index));
jumps_need_update = false;