bug#38485: Customizing glyph widths

[Clément Pit-Claudel]

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

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 :/