scale with the given size (default 16). This can be put in the site.def or .magicrc file as, e.g., "set Opts(toolsize) 32". This is the first part of an attempt to get everything to scale properly on ultra-high- resolution monitors.