Fix the values of HEADER_MARGIN and HEADER_EXTRA #411
Description
The Tree.HEADER_MARGIN and Tree.HEADER_EXTRA constant defines extra fixed-width spacing for tree headers. Previously, this was a fixed pixel value, which worked at 100% zoom but did not scale properly on high-DPI monitors.