bug#38485: Customizing glyph widths

[Clément Pit-Claudel]

On 2019-12-04 22:34, Eli Zaretskii wrote:
>> Cc: casouri@gmail.com, 38485@debbugs.gnu.org
>> From: Clément Pit-Claudel <cpitclaudel@gmail.com>
>> Date: Wed, 4 Dec 2019 15:53:43 -0500
>>
>>> No, it will simply make each prettified symbol take up the same width
>>> as the original characters of the symbol that were composed.  Isn't
>>> that what everyone would want, and want for _all_ prettified symbols?
>>
>> Probably not.  In proof-general, we display 'forall' as ∀ and 'exists' as ∃. 
>>  In my own configuration I also change "Qed" to ■ "Defined" to □, and 
>> "Admitted" to 😱.  These shouldn't be widened, I think — especially not the 
>> last ones (there is a case to be made for widening forall, since otherwise 
>> we might get indentation issues, but in Coq Qed, Defined and Admitted don't 
>> introduce indentation changes, so it's safe not to widen them.
> 
> 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.

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. □      .

Clément.