[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Variable pitch mode line
From: |
Juri Linkov |
Subject: |
Re: Variable pitch mode line |
Date: |
Fri, 24 Dec 2021 10:21:59 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/29.0.50 (x86_64-pc-linux-gnu) |
>> I don't believe that distro packagers might want to include Info manuals
>> in the HTML format when only Emacs will display them but not the standalone
>> Info reader.
>
> I'm not sure they include Info manuals mainly for the standalone info
> viewer either. But in any case, currently I don't think any doc viewer
> has a good story for "use HTML as replacement for Info", so it's clear
> that if we want it to happen, we need to start by making Emacs support
> it well. And only later, *maybe*, distros and other Info viewers will
> follow suit.
Then better to start with own dog food, and first display Emacs manuals
from HTML. There is already a make target that produces HTML files:
make html
Currently HTML files are generated in the source dir, that is wrong:
doc/emacs/emacs.html
The correct place would be in the Info output dir:
info/emacs.html
so it could reuse INFOPATH to find HTML Info manuals as well.
Then after visiting the generated HTML with eww, when proportional fonts
are enabled with `eww-toggle-fonts`, the output looks nice.
But rendering a large HTML file takes too much time. So while
a single HTML file is still preferable over multifile Info manuals,
the Info reader should limit rendering to the currently displayed
Info node only.
Using a single HTML file will also make online reading of remote HTML
manuals easier. For example, simply point the Emacs Info reader to
https://www.gnu.org/software/emacs/manual/html_mono/emacs.html
and it could fetch the whole HTML file, then navigate its nodes.
- Re: HTML info, (continued)
- Re: HTML info, Juri Linkov, 2021/12/25
- Re: HTML info, Yuan Fu, 2021/12/26
- Re: HTML info, Eli Zaretskii, 2021/12/26
- Re: HTML info, Lars Ingebrigtsen, 2021/12/26
- Re: HTML info, Eli Zaretskii, 2021/12/26
- Re: HTML info, Lars Ingebrigtsen, 2021/12/26
- Re: HTML info, Eli Zaretskii, 2021/12/26
- Re: Variable pitch mode line,
Juri Linkov <=
- 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, 2021/12/24
- 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