bug#37667: 27.0.50; Tab Bar display problems with more than 5 tabs

[Eli Zaretskii]

> From: Juri Linkov <juri@linkov.net>
> Cc: rudalics@gmx.at,  37667@debbugs.gnu.org
> Date: Mon, 14 Oct 2019 23:07:50 +0300
> 
> >> I tried a variable-pitch font for tab bars, and it looks good
> >> and makes tab widths smaller, so more tabs fits into the tab-bar.
> >
> > Could be a good idea.  Toolkit menu bars definitely use variable-pitch
> > fonts on most systems.
> 
> So I changed tab bars to use variable-pitch fonts.

Please make the :height attribute smaller, like 0.9.  The current
value of 1.1 produces too large tab names.

Btw, as long as we are optimizing the tab-bar appearance: I think the
choice of the colors of the current and non-current tabs should be
reversed: the lighter color is more appropriate for "inactive" than
the darker one.  Alternatively, use some non-gray color for the
current tab (I personally think these gray colors are too dull).

Thanks.