Subject: bug#38485: Customizing glyph widths

From: Clément Pit-Claudel <[email-masked]>
Date: Thu, 5 Dec 2019 14:50:54 -0500

On 2019-12-05 10:19, Eli Zaretskii wrote:
>> Cc: [email-masked], [email-masked]
>> From: Clément Pit-Claudel <[email-masked]>
>> 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 :/