[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Adding a "quick-help" menu
From: |
Stefan Kangas |
Subject: |
Re: Adding a "quick-help" menu |
Date: |
Mon, 17 Oct 2022 05:10:25 +0000 |
Philip Kaludercic <philipk@posteo.net> writes:
>> - I think we should use `help-for-help-header' for the headlines, not
>> capitalize them, and align them with :align-to.
>
> That can be done.
I note that you did not use the `help-for-help-header' face for the
headlines. They are also manually aligned, not with :align-to.
I tried with this naive patch, which means that alignment is off, but
the results look promising to me:
diff --git a/lisp/help.el b/lisp/help.el
index 1cfd044db8..3979d772bc 100644
--- a/lisp/help.el
+++ b/lisp/help.el
@@ -197,7 +197,7 @@ help-quick
(concat
(car section)
(make-string (- width (length (car section))) ?\s))
- 'face 'bold)
+ 'face 'help-for-help-header)
,@(mapcar (lambda (ent)
(format fmt
(propertize
In any case, I don't think using the face `bold' is best here, as that
makes this hard to customize. I'd prefer a proper defface (whether it
inherits from `help-for-help-header' by default or not).
- Re: Adding a "quick-help" menu, (continued)
- Re: Adding a "quick-help" menu, Philip Kaludercic, 2022/10/16
- Re: Adding a "quick-help" menu, Howard Melman, 2022/10/16
- Re: Adding a "quick-help" menu, Philip Kaludercic, 2022/10/16
- RE: [External] : Re: Adding a "quick-help" menu, Drew Adams, 2022/10/16
- Re: Adding a "quick-help" menu, Howard Melman, 2022/10/17
- Re: Adding a "quick-help" menu, Eli Zaretskii, 2022/10/17
- Re: Adding a "quick-help" menu, Philip Kaludercic, 2022/10/17
- Re: Adding a "quick-help" menu, Eli Zaretskii, 2022/10/17
- Re: Adding a "quick-help" menu, Stefan Kangas, 2022/10/17
- Re: Adding a "quick-help" menu, Howard Melman, 2022/10/17
Re: Adding a "quick-help" menu,
Stefan Kangas <=
- Re: Adding a "quick-help" menu, Philip Kaludercic, 2022/10/17
- Re: Adding a "quick-help" menu, Protesilaos Stavrou, 2022/10/20
- Re: Adding a "quick-help" menu, Eli Zaretskii, 2022/10/20
- Re: Adding a "quick-help" menu, Philip Kaludercic, 2022/10/20
- Re: Adding a "quick-help" menu, Eli Zaretskii, 2022/10/20
- Re: Adding a "quick-help" menu, Philip Kaludercic, 2022/10/20
- Re: Adding a "quick-help" menu, Eli Zaretskii, 2022/10/20