149     // | console.log("Entering state «@name»", this.frequency);

   149     // | console.log("Entering state «@name»", this.frequency);

   150     apply "*", mode="actions";

   150     apply "*", mode="actions";

   151     |     }

   151     |     }

   152 }

   152 }

   153 template "show", mode="actions" {

   153 template "show", mode="actions" {

   155     |         this.request_animate();

   155     |         this.request_animate();

   156 }

   156 }

   157 template "hmi-value", mode="actions" {

   157 template "hmi-value", mode="actions" {

   158     |         this.apply_hmi_value(0, «@value»);

   158     |         this.apply_hmi_value(0, «@value»);

   159 }

   159 }

   162 

   162 

   163 

   163 

   164 function "generated_button_class" {

   164 function "generated_button_class" {

   165     param "fsm";

   165     param "fsm";

   166 

   166 

   168     |     state = "init";

   167     |     state = "init";

   169 

   168 

   170     |     dispatch(value) {

   169     |     dispatch(value) {

   171     apply "$fsm", mode="dispatch_transition";

   170     apply "$fsm", mode="dispatch_transition";

   172     |     }

   171     |     }

   180     apply "$fsm", mode="mouse_transition" with "position", "'down'";

   179     apply "$fsm", mode="mouse_transition" with "position", "'down'";

   181     |     }

   180     |     }

   182 

   181 

   183     apply "$fsm", mode="actions";

   182     apply "$fsm", mode="actions";

   184 

   183 

   189     |     init() {

   184     |     init() {

   190     |         this.bound_onmouseup = this.onmouseup.bind(this);

   185     |         this.bound_onmouseup = this.onmouseup.bind(this);

   191     |         this.element.addEventListener("pointerdown", this.onmousedown.bind(this));

   186     |         this.element.addEventListener("pointerdown", this.onmousedown.bind(this));

   193     |     }

   188     |     }

   194 }

   189 }

   195 

   190 

   196 

   191 

   197 widget_class("Button"){

   192 widget_class("Button"){