Scroll-bars used to draw in a little extra space in the editor, causing
buttons to jump a bit when they appeared/disappeared. Now they draw on
top of the buttons, just small enough to avoid bigger overlaps. Followup commits
will do further adjustments.
With this we can get rid of a hack that was calling the (often Python
defined) panel definition - the panel 'draw' callback - twice.
4ec467d3b5