Re: Bug in mouse highlighting

[Kim F. Storm]

Stephen Berman <address@hidden> writes:

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

I don't know -- and I don't really want to think about it.
Things seem to work now, that's good enough for me :-)

-- 
Kim F. Storm <address@hidden> http://www.cua.dk