[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#60587: Patch for adding links to symbols' help documentation
From: |
Eli Zaretskii |
Subject: |
bug#60587: Patch for adding links to symbols' help documentation |
Date: |
Sat, 28 Jan 2023 10:11:18 +0200 |
> From: Drew Adams <drew.adams@oracle.com>
> CC: Eli Zaretskii <eliz@gnu.org>,
> "60587@debbugs.gnu.org"
> <60587@debbugs.gnu.org>,
> "monnier@iro.umontreal.ca"
> <monnier@iro.umontreal.ca>
> Date: Fri, 27 Jan 2023 23:13:36 +0000
>
> > > 5. Face `info-color' should be named something like
> > > `info-symbol-help-link'.
> >
> > You're right, `info-color' is too minimalist and not describing what the
> > object represents.
> >
> > (I dropped it completely because I realised an additional face is
> > redundant since Info distinguishes (slightly) quoted symbols from the
> > text, anyway.)
>
> I think it's _good_ to have a separate face for this.
I disagree that another face is a Good Thing. We have too many of
them already.
> That gives users the choice:
>
> * Have the same appearance for both kinds of link.
> * Have the two kinds of link (Info, *Help*) look
> different.
>
> When you provide two faces, users can always customize
> them to look the same, if they like. Otherwise, they
> don't have that possibility.
The downside of having a separate face is the need to know about it
and customize it separately. So an additional face is not just an
advantage, it is also a disadvantage. Thus, we should introduce new
faces only if they really are for a different purpose. This one
isn't.
- bug#60587: Patch for adding links to symbols' help documentation, (continued)
- bug#60587: Patch for adding links to symbols' help documentation, H. Dieter Wilhelm, 2023/01/25
- bug#60587: Patch for adding links to symbols' help documentation, Drew Adams, 2023/01/25
- bug#60587: Patch for adding links to symbols' help documentation, Ihor Radchenko, 2023/01/26
- bug#60587: Patch for adding links to symbols' help documentation, Drew Adams, 2023/01/26
- bug#60587: Patch for adding links to symbols' help documentation, Ihor Radchenko, 2023/01/26
- bug#60587: Patch for adding links to symbols' help documentation, Drew Adams, 2023/01/26
- bug#60587: Patch for adding links to symbols' help documentation, H. Dieter Wilhelm, 2023/01/27
- bug#60587: Patch for adding links to symbols' help documentation, Stefan Monnier, 2023/01/27
- bug#60587: Patch for adding links to symbols' help documentation, Drew Adams, 2023/01/27
- bug#60587: Patch for adding links to symbols' help documentation, Drew Adams, 2023/01/27
- bug#60587: Patch for adding links to symbols' help documentation,
Eli Zaretskii <=
- bug#60587: Patch for adding links to symbols' help documentation, Drew Adams, 2023/01/28
- bug#60587: Patch for adding links to symbols' help documentation, Eli Zaretskii, 2023/01/26
- bug#60587: Patch for adding links to symbols' help documentation, Juri Linkov, 2023/01/27
- bug#60587: Patch for adding links to symbols' help documentation, Eli Zaretskii, 2023/01/27
- bug#60587: Patch for adding links to symbols' help documentation, H. Dieter Wilhelm, 2023/01/27
- bug#60587: Patch for adding links to symbols' help documentation, Eli Zaretskii, 2023/01/28