[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Variable-width font indentation
From: |
Eli Zaretskii |
Subject: |
Re: Variable-width font indentation |
Date: |
Fri, 09 Mar 2018 20:35:05 +0200 |
> Cc: address@hidden
> From: Paul Eggert <address@hidden>
> Date: Fri, 9 Mar 2018 09:52:28 -0800
>
> If the objection is that different blocks of code are indented
> differently (e.g., an if-part might be indented slightly differently
> from the corresponding then-part), then I agree that might irritate some
> users. However, the irritation is quite small to me, and I imagine it
> wouldn't bother other users much either
Well, it bothers me a lot, to the degree that I don't think it could
fly.
> Of course other display algorithms are possible, but I haven't seen any
> other improvement proposed for variable-pitch fonts that is nearly as
> simple and easy to understand. Simplicity is a virtue here.
Simplicity is a virtue if it gets the job done. This particular
suggestion doesn't, IMO.
- Re: Variable-width font indentation, (continued)
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/07
- Re: Variable-width font indentation, Clément Pit-Claudel, 2018/03/07
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/07
- Re: Variable-width font indentation, Clément Pit-Claudel, 2018/03/07
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/08
- Re: Variable-width font indentation, Clément Pit-Claudel, 2018/03/08
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/08
- Re: Variable-width font indentation, Clément Pit-Claudel, 2018/03/08
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/09
- Re: Variable-width font indentation, Paul Eggert, 2018/03/09
- Re: Variable-width font indentation,
Eli Zaretskii <=
- Re: Variable-width font indentation, Paul Eggert, 2018/03/09
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/09
- Re: Variable-width font indentation, Paul Eggert, 2018/03/09
- Re: Variable-width font indentation, James Cloos, 2018/03/09
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/10
- Re: Variable-width font indentation, James Cloos, 2018/03/10
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/10
- Re: Variable-width font indentation, James Cloos, 2018/03/10
- Re: Variable-width font indentation, Eli Zaretskii, 2018/03/10
- Re: Variable-width font indentation, Clément Pit-Claudel, 2018/03/09