Also includes general improvements to the slider widget such as an optional
"autotrim" function to cut off trailing zeroes, a "format" string that's easier
to internationalize, and general tidiness.
A slider can now hold a float value and display it in the UI converted to
either a percentage or a decibel (still returning a linear float value
programmatically for the rest of the code).