e872a5e Use CSS-like defaulting of text-box margins