14     

    14     

    15 }

    15 }

    16 

    16 

    17 widget_class("Slider")

    17 widget_class("Slider")

    18     ||

    18     ||

    20         frequency = 5;

    19         frequency = 5;

    21         range = undefined;

    20         range = undefined;

    22         handle_orig = undefined;

    21         handle_orig = undefined;

    23         scroll_size = undefined;

    22         scroll_size = undefined;

    24         scroll_range = 0;

    23         scroll_range = 0;

   348                 this.setpoint_style = this.setpoint_elt.getAttribute("style");

   347                 this.setpoint_style = this.setpoint_elt.getAttribute("style");

   349                 this.setpoint_elt.setAttribute("style", "display:none");

   348                 this.setpoint_elt.setAttribute("style", "display:none");

   350             }

   349             }

   351 

   350 

   352         }

   351         }

   354     ||

   352     ||

   355 

   353 

   356 widget_defs("Slider") {

   354 widget_defs("Slider") {

   357     labels("handle range");

   355     labels("handle range");

   358     optional_labels("value min max setpoint");

   356     optional_labels("value min max setpoint");