[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#38485: Customizing glyph widths
From: |
Eli Zaretskii |
Subject: |
bug#38485: Customizing glyph widths |
Date: |
Thu, 05 Dec 2019 17:19:19 +0200 |
> Cc: casouri@gmail.com, 38485@debbugs.gnu.org
> From: Clément Pit-Claudel <cpitclaudel@gmail.com>
> Date: Thu, 5 Dec 2019 09:26:12 -0500
>
> > Are you saying that we _can_ not widen them, or are you saying that we
> > _must_not_ widen them? If the latter, can you explain why not?
>
> That we must not. I set up these prettifications specifically to make the
> characters narrower and reduce visual clutter; widening them would defeat
> that purpose.
So in this case the alignment considerations are thrown out the
window?
> I commonly write things like this:
>
> Lemma lcomm: forall x y, x ~+~ y <-> y ~+~ x.
> Proof. induction x; cbn; try rewrite IHx; reflexivity. Defined.
>
> with prettification, it looks like this:
>
> Lemma lcomm: ∀ x y, x ⨤ y ↔ y ⨤ x.
> ∵. induction x; cbn; try rewrite IHx; reflexivity. □.
>
> What I really want is this:
>
> Lemma lcomm: ∀ x y, x ⨤ y ↔ y ⨤ x.
> ∵. induction x; cbn; try rewrite IHx; reflexivity. □.
>
> but not this:
>
> Lemma lcomm: ∀ x y, x ⨤ y ↔ y ⨤ x.
> ∵ . induction x; cbn; try rewrite IHx; reflexivity. □ .
Why is "Proof" treated differently from the other symbols? How would
the user know which one is which?
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/03
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: Customizing glyph widths,
Eli Zaretskii <=
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/05
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: "prettified" symbols, Richard Stallman, 2019/12/05
- bug#38485: "prettified" symbols, Eli Zaretskii, 2019/12/06
- bug#38485: "prettified" symbols, Richard Stallman, 2019/12/06
- bug#38485: "prettified" symbols, Clément Pit-Claudel, 2019/12/06
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05