Let sliders in number widget support floating point numbers

[imagejan]

This allows to use non-integer step sizes and ranges in script parameters with style="slider" (see #31).

#@ Integer (style="slider", min=0, max=100, stepSize=2) a
#@ Double (style="slider", min=0, max=100, stepSize=1.5) b
#@ Double (style="slider", min=0, max=100, stepSize=20) c
#@ Double (style="slider", min=0, max=1, stepSize=0.1) d
#@ Double (style="slider", min=-10, max=5, stepSize=5) e
#@ Double (style="slider", min=-0.03, max=0.05, stepSize=0.001) f

Remaining issues:

• the preferred width of the sliders messes up the alignment and squeezes the text fields too much
• scroll bars still only support integers
• sometimes I noticed strange behavior of the slider when range << 1 and trying to adjust the value; it seems to snap to 0 (may be related to Spinner increment/decrement precision problem #19)

[imagejan]

I fixed the remaining issues by:

• setting a default preferred size for spinners in the widget
• applying the same logic as for sliders to scroll bars (private nested class CalibratedScrollBar)
• fixing a few instances where getValue().intValue() was used.

@ctrueden this PR is ready to be merged from my side.

[ctrueden]

@imagejan You are a rock star! 🎸