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.
I think this should be `^\s*([+-]?\d*\.?\d?)\s*[-:]\s*([+-]?\d*\.?\d?)` which allows the python shorthand float declaration, i.e. `1.-2.`.