[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: |
Thu, 23 Dec 2021 21:45:27 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/29.0.50 (x86_64-pc-linux-gnu) |
>>> BTW: I would love to have pixel-filled, variable pitch info docs.
>>> `variable-pitch-mode' in info has the bad effect that also code
>>> samples or ASCII art [like the cons box&arrows in (info "(elisp)
>>> Building Lists")] then use the variable pitch font and misalign.
>>
>> The only way to reliably support variable pitch in the Info reader is
>> by using HTML output from Texinfo and rendering it with eww/shr.
>
> What's the problem with info? I mean, we use special environments such
> as `@example ... @end example` in order to mark non-prose text in the
> texi files. Right now, they seem to only add some indentation in the
> info files. But couldn't makeinfo add some hints (like some invisible
> chars) so that info readers could detect such non-prose text?
Texinfo already adds invisible markers to the index and images,
so it could output more invisible markup indeed.
- Re: Variable pitch mode line, (continued)
- Re: Variable pitch mode line, Stefan Monnier, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line, Stefan Monnier, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- HTML info, Yuan Fu, 2021/12/23
- Re: Variable pitch mode line, Tassilo Horn, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line, Tassilo Horn, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/23
- Re: Variable pitch mode line,
Juri Linkov <=
- Re: Variable pitch mode line, Tomas Hlavaty, 2021/12/23
- Re: Variable pitch mode line, Yuan Fu, 2021/12/23
- Re: Variable pitch mode line, Tomas Hlavaty, 2021/12/23
- Re: Variable pitch mode line, Yuan Fu, 2021/12/23
- Re: Variable pitch mode line, Tomas Hlavaty, 2021/12/23
- Re: Variable pitch mode line, Yuan Fu, 2021/12/23
- Re: Variable pitch mode line, Tomas Hlavaty, 2021/12/23
- Re: Variable pitch mode line, Yuan Fu, 2021/12/23
- Re: Variable pitch mode line, Tomas Hlavaty, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24