Re: Bug in mouse highlighting

[Stephen Berman]

On Wed, 10 Nov 2004 10:12:33 +0100 address@hidden (Kim F. Storm) wrote:

> Stephen Berman <address@hidden> writes:
>
>> I also have a related question, which I'm very curious to know the
>> answer to: as I mentioned in my bug report, the "bleeding" didn't
>> happen in Info, with the Info header line, and I couldn't figure out
>> what makes it different from other header lines (at least the ones I
>> defined myself and in e.g. tabbar-mode).  Do you (or anyone else
>> reading this) know?
>
> Strange -- but maybe the header line font is slightly smaller than the
> text line you scroll out of view (behind the header line) -- in which
> case there is no "hidden" line that can bleed into the header line.

I don't follow you: What hidden line is there beside the one that is
scrolled behind the header line and how does the difference in font
size stop it from being hidden?  The line that's scrolled behind the
header is not visible, or do you mean something else by "hidden"?  It
sounds like you're suggesting that with a header line font which is
slightly smaller that the text font, there shouldn't be this bleeding.
But it appears that this makes no difference: When I enable the tab
bar it has a default face with a height of scale 0.8, but whether I
use this or make the height the same as the text font, the bleeding
occurs (in the absence of your fix, of course!).  In contrast, in
Info, where the bleeding doesn't occur, the header line and text have
the same font by default.