GNU bug report logs - #38485
Customizing glyph widths

Previous Next

Full log

Message #47 received at 38485 <at> debbugs.gnu.org (full text, mbox):

From: Clément Pit-Claudel <cpitclaudel <at> gmail.com>
To: Eli Zaretskii <eliz <at> gnu.org>
Cc: casouri <at> gmail.com, 38485 <at> debbugs.gnu.org
Subject: Re: bug#38485: Customizing glyph widths
Date: Thu, 5 Dec 2019 14:50:54 -0500

On 2019-12-05 10:19, Eli Zaretskii wrote:
>> 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?

Yes; for 'forall' it's debatable, but for Qed, Defined and Admitted it's safe to not widen them, because they don't introduce indentation points.

>> 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?

Sorry, I think I don't understand the question :/

Previous Next

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