[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: facemenu-unlisted-faces

From: Richard Stallman
Subject: Re: facemenu-unlisted-faces
Date: Wed, 05 Jul 2006 10:51:27 -0400

    It is far more natural to click Bold a second time to turn off boldness for
    the selection than it is to think of applying the `default' face to it.

That is a good idea.  However, this is not the same as what you were
talking about before.  This is an interface question.  You were
talking about a conceptual quesion, whether to consider it a "face" or
a "face attribute".

    The fact that face named "fixed pitch" has a fixed pitch is
    a happy happenstance.

It is not happenstance.  That's what the name is meant to be used for.

                          It is the monospace (fixed pitch) font property that a
    user wants to apply to text in this case,

There is no such "font property".  Some fonts are fixed pitch, and
some are not.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]