auctex-devel
[Top][All Lists]
Advanced

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

[AUCTeX-devel] Re: Fontifying of titles...


From: Ralf Angeli
Subject: [AUCTeX-devel] Re: Fontifying of titles...
Date: Tue, 05 Apr 2005 08:49:12 +0200
User-agent: Gnus/5.110003 (No Gnus v0.3) Emacs/22.0.50 (gnu/linux)

* David Kastrup (2005-04-05) writes:

> Ralf Angeli <address@hidden> writes:
>
>> and don't think that the suggestions will improve it in any way
>
> I can't see how providing an easily accessible option for turning it
> off if desired could be bad.

It will unnecessarily clutter the menu because it is an option used
once in a lifetime.  And unless you are thinking of writing directly
to the init file when changing the option, you have to provide an
additional menu entry for saving, like it is done in Emacs' "Options"
menu.  Mentioning the variable to be changed in the help echo could be
a less convenient compromise.

We have several options which can be set temporarily from the menu and
for which there is no way to set their default permanently from the
menu.  For most of them this is not a big deal because they are
switched more often.  Some of them, like fold mode or math mode might
warrant the provision of a way to save them.

This is a personal opinion, but I've never used the "Save Options"
menu entry because I didn't really know what it does.  For example,
will it clutter my init file with an entry for every option in the
menu?  It probably won't, but who knows.  The options menu as a whole
just feels awkward.  Every other application has a single menu entry
for firing up a customization dialog.  The "Options" menu looks like a
poor-man's version of this.

>> and I am strongly against changing it.
>
> It would probably worth doing a poll on the AUCTeX list in order to
> get more qualified numbers here.  It is clear that our guesses about
> the public opinion are quite different.  Doing a poll will not change
> our personal preferences, but will make it better possible to see how
> relevant they might be to the user base.

I am not really a fan of such polls.  Especially if there is only a
smaller audience they tend to be distorted and not representative.
But for the sake of finding a conclusion here we might as well give it
a try.

-- 
Ralf





reply via email to

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