[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Variable pitch mode line
From: |
Lars Ingebrigtsen |
Subject: |
Re: Variable pitch mode line |
Date: |
Fri, 24 Dec 2021 13:53:55 +0100 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/29.0.50 (gnu/linux) |
Po Lu <luangruo@yahoo.com> writes:
> I haven't had the time to read through this thread, but can someone
> assure me that the existing Info format and reader will remain, and that
> Emacs documentation will continue to be generated in that format?
Yes, the Emacs documentation will continue to be available in all the
formats that Texinfo supports.
> I also don't understand how an HTML-based Info reader will handle (for
> example) I-search through an entire manual without rendering it all in
> one go.
We don't have to render the HTML to search in it -- parsing the HTML is
enough (and is quick), and then we can just search in the DOM and then
render the node we find the match in. It's just a small matter of
programming.
--
(domestic pets only, the antidote for overdose, milk.)
bloggy blog: http://lars.ingebrigtsen.no
- HTML info, (continued)
- HTML info, Yuan Fu, 2021/12/23
- Re: HTML info, Juri Linkov, 2021/12/24
- Re: HTML info, Eli Zaretskii, 2021/12/24
- Re: HTML info, Lars Ingebrigtsen, 2021/12/24
- Re: HTML info, Po Lu, 2021/12/24
- Re: Variable pitch mode line, Juri Linkov, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24
- Re: Variable pitch mode line, Lars Ingebrigtsen, 2021/12/24
- Re: Variable pitch mode line, Po Lu, 2021/12/24
- Re: Variable pitch mode line,
Lars Ingebrigtsen <=
- Re: Variable pitch mode line, Po Lu, 2021/12/24
- Re: Variable pitch mode line, Lars Ingebrigtsen, 2021/12/24
- Re: Variable pitch mode line, Po Lu, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24
- Re: Variable pitch mode line, Lars Ingebrigtsen, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24
- Re: Variable pitch mode line, Lars Ingebrigtsen, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24
- Re: Variable pitch mode line, Lars Ingebrigtsen, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24