From: Eli Zaretskii <eliz@gnu.org>
To: "Clément Pit-Claudel" <cpitclaudel@gmail.com>
Cc: casouri@gmail.com, 38485@debbugs.gnu.org
Subject: bug#38485: Customizing glyph widths
Date: Thu, 05 Dec 2019 17:19:19 +0200 [thread overview]
Message-ID: <83a786iyvc.fsf@gnu.org> (raw)
In-Reply-To: <f7618005-6017-cd8d-423b-d4fb6df8bc08@gmail.com> (message from Clément Pit-Claudel on Thu, 5 Dec 2019 09:26:12 -0500)
> 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?
> 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?
next prev parent reply other threads:[~2019-12-05 15:19 UTC|newest]
Thread overview: 21+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-12-04 4:22 bug#38485: Customizing glyph widths Clément Pit-Claudel
2019-12-04 15:52 ` Eli Zaretskii
2019-12-04 16:57 ` Clément Pit-Claudel
2019-12-04 17:05 ` Eli Zaretskii
2019-12-04 18:14 ` Clément Pit-Claudel
2019-12-04 18:45 ` Eli Zaretskii
2019-12-04 20:53 ` Clément Pit-Claudel
2019-12-05 3:34 ` Eli Zaretskii
2019-12-05 14:26 ` Clément Pit-Claudel
2019-12-05 15:19 ` Eli Zaretskii [this message]
2019-12-05 19:50 ` Clément Pit-Claudel
2019-12-05 20:06 ` Eli Zaretskii
2019-12-05 20:53 ` Clément Pit-Claudel
2019-12-06 4:15 ` bug#38485: "prettified" symbols Richard Stallman
2019-12-06 5:51 ` Clément Pit-Claudel
2019-12-06 7:58 ` Eli Zaretskii
2019-12-07 4:42 ` Richard Stallman
2019-12-04 20:55 ` bug#38485: Customizing glyph widths Clément Pit-Claudel
2019-12-05 3:36 ` Eli Zaretskii
2019-12-05 14:29 ` Clément Pit-Claudel
2019-12-05 3:57 ` Yuan Fu
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=83a786iyvc.fsf@gnu.org \
--to=eliz@gnu.org \
--cc=38485@debbugs.gnu.org \
--cc=casouri@gmail.com \
--cc=cpitclaudel@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/emacs.git
https://git.savannah.gnu.org/cgit/emacs/org-mode.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.