this implements the first version of #36 and #37, in which the brush size picker is a numeric input field rather than a slider.