GNU bug report logs - #38485
Customizing glyph widths

Previous Next

Full log

View this message in rfc822 format

From: Eli Zaretskii <eliz <at> gnu.org>
To: Clément Pit-Claudel <cpitclaudel <at> gmail.com>
Cc: casouri <at> gmail.com, 38485 <at> debbugs.gnu.org
Subject: bug#38485: Customizing glyph widths
Date: Thu, 05 Dec 2019 17:19:19 +0200

> Cc: casouri <at> gmail.com, 38485 <at> debbugs.gnu.org
> From: Clément Pit-Claudel <cpitclaudel <at> 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?

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.