[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Variable pitch mode line
From: |
Tomas Hlavaty |
Subject: |
Re: Variable pitch mode line |
Date: |
Thu, 23 Dec 2021 22:24:06 +0100 |
On Thu 23 Dec 2021 at 13:00, Yuan Fu <casouri@gmail.com> wrote:
>> On Dec 23, 2021, at 12:56 PM, Tomas Hlavaty <tom@logand.com> wrote:
>> On Thu 23 Dec 2021 at 12:51, Yuan Fu <casouri@gmail.com> wrote:
>>> I’ve tried that. Info files are not complex, but they can’t be
>>> reliably parsed 100% of the time. My code works for like 95% of the
>>> nodes, but there are always some corner cases where it breaks.
>>
>> Why doesn't texinfo html output suffer from this problem?
>
> HTML are structured, where as Info is more like plain text. Just to
> give an example, in an info file, four spaces indent text could be a
> code block, or just an indented paragraph, there is no way telling
> them apart. In HTML, code is wrapped in <code> (or maybe <pre>),
> paragraphs are wrapped in <p>.
Sorry for not being clearer.
The question is not about the difference between info and html.
The question is: why does your info to html conversion attempt work in
95% cases but textinfos info to html conversion work in 100% cases?
- Re: Variable pitch mode line, (continued)
- 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, 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 <=
- 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
- RE: [External] : Re: Variable pitch mode line, Drew Adams, 2021/12/23
- Re: [External] : Re: Variable pitch mode line, Yuan Fu, 2021/12/23
- RE: [External] : Re: Variable pitch mode line, Drew Adams, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24
- Re: Variable pitch mode line, Eli Zaretskii, 2021/12/24