Re: header-line-format vs. window fringes

[Richard M. Stallman]

    I don't know how to do that when the window has non-null fringes,
    because I know the fringes' widths, but I don't see a way to know the
    width of the monospaced font, in pixels.

The fringes always occupy an even multiple of a "column",
which I believe is the width of space in the default font.
So you could just use the right number of spaces.
But how many spaces?  You could divide left-fringe-width
with the value returned by frame-char-width.
I think that should work.  Doesn't it work?

The doc string of frame-char-width seems to be out of date.
I think this is what it should say.


       doc: /* Width in pixels of characters in the font in frame FRAME.
If FRAME is omitted, the selected frame is used.
On a graphical screen, the width is the standard width of the default font.
For a terminal screen, the value is always 1.  */)