Allow text input on slider widgets

This adds "click-to-edit" to the text readout to the right of a slider, allowing precise values to be set.

Changes are entirely on the javascript. Editing is handled using the HTML5 `contentEditable` attribute rather than explicitly creating any input widget. The modified value is committed by either clicking outside the text, or pressing enter. Works for both `Int` and `FloatSliderView`.

The new value is validated for float/int and min/max, but the step size (if set) is not enforced.

This will need updating if #6050 is merged.
As written this matches a lone decimal point, and does not match numbers with >1 decimal place - but I agree with the point. I'll fix it so it matches `1.`.