>> >> 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.

So I changed :height to 0.9 (tab-line tabs should have
smaller height because they are more local).

> 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).

The current color scheme is the same as used in Web browsers where the
current tab has the lighter color, so users are accustomed to such
palette.  Here is comparison of colors (at the bottom is Chromium):