From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!.POSTED.blaine.gmane.org!not-for-mail From: =?UTF-8?Q?Cl=C3=A9ment?= Pit-Claudel Newsgroups: gmane.emacs.bugs Subject: bug#38485: Customizing glyph widths Date: Thu, 5 Dec 2019 14:50:54 -0500 Message-ID: <5b3d638e-5913-2c3d-dba1-0c3f387a7ff2@gmail.com> References: <3183ba6c-6aea-fa25-bb32-7e5ff7c04ad6@gmail.com> <83y2vshyvn.fsf@gnu.org> <478afae1-0080-c825-5a53-1bc8e897a1cc@gmail.com> <83sgm0hvhx.fsf@gnu.org> <4e6c87d3-21c0-1820-96f2-62bb0dd7c925@gmail.com> <83r21khquw.fsf@gnu.org> <32a6f122-f21a-4522-21d6-0ae0a17b6bee@gmail.com> <83o8wnigy5.fsf@gnu.org> <83a786iyvc.fsf@gnu.org> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Injection-Info: blaine.gmane.org; posting-host="blaine.gmane.org:195.159.176.226"; logging-data="255623"; mail-complaints-to="usenet@blaine.gmane.org" User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.2.1 Cc: casouri@gmail.com, 38485@debbugs.gnu.org To: Eli Zaretskii Original-X-From: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Thu Dec 05 20:52:14 2019 Return-path: Envelope-to: geb-bug-gnu-emacs@m.gmane.org Original-Received: from lists.gnu.org ([209.51.188.17]) by blaine.gmane.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.89) (envelope-from ) id 1icxAb-0014Mk-Nd for geb-bug-gnu-emacs@m.gmane.org; Thu, 05 Dec 2019 20:52:13 +0100 Original-Received: from localhost ([::1]:60358 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1icxAa-00071c-Jk for geb-bug-gnu-emacs@m.gmane.org; Thu, 05 Dec 2019 14:52:12 -0500 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:53646) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1icxAR-0006xD-BZ for bug-gnu-emacs@gnu.org; Thu, 05 Dec 2019 14:52:04 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1icxAQ-0007ge-3I for bug-gnu-emacs@gnu.org; Thu, 05 Dec 2019 14:52:03 -0500 Original-Received: from debbugs.gnu.org ([209.51.188.43]:39262) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1icxAP-0007f5-Qg for bug-gnu-emacs@gnu.org; Thu, 05 Dec 2019 14:52:01 -0500 Original-Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1icxAP-0002Lg-OO for bug-gnu-emacs@gnu.org; Thu, 05 Dec 2019 14:52:01 -0500 X-Loop: help-debbugs@gnu.org Resent-From: =?UTF-8?Q?Cl=C3=A9ment?= Pit-Claudel Original-Sender: "Debbugs-submit" Resent-CC: bug-gnu-emacs@gnu.org Resent-Date: Thu, 05 Dec 2019 19:52:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38485 X-GNU-PR-Package: emacs Original-Received: via spool by 38485-submit@debbugs.gnu.org id=B38485.15755754638950 (code B ref 38485); Thu, 05 Dec 2019 19:52:01 +0000 Original-Received: (at 38485) by debbugs.gnu.org; 5 Dec 2019 19:51:03 +0000 Original-Received: from localhost ([127.0.0.1]:45235 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1icx9T-0002KI-7Q for submit@debbugs.gnu.org; Thu, 05 Dec 2019 14:51:03 -0500 Original-Received: from mail-qv1-f52.google.com ([209.85.219.52]:40979) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1icx9R-0002Jm-J6 for 38485@debbugs.gnu.org; Thu, 05 Dec 2019 14:51:02 -0500 Original-Received: by mail-qv1-f52.google.com with SMTP id b18so1761979qvo.8 for <38485@debbugs.gnu.org>; Thu, 05 Dec 2019 11:51:01 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding; bh=p6fXN/zS/zND2SpdY9qTubGL39E++nU1YObZB7P105c=; b=tvhpwQ/HCMQbkTsXfXpzJ4ntpnDuORqaujpxokDsxWMpAD4Fx75GpgVjgYKkIoc5iA qPLdnezHASft31slbw8H027jeAggdFoBaovvltOZc8kOmx+PFGxavN6sUz75s0UBFn22 RfmFpscI0NGgqrGELpmPXAsq7yjF7Fl90bcQe7F09aeMP9abcarpreAG04EnoRGcAfdT fj946ptyaukCnvjKmkwLI4WAE3CuWF8BybTHl/005WsfINyH2MZaWsshr9PARfRV1BNU 6FzxOCn9jLgARwQmtaY9LVQQFEhAvylvNFqkti2qsxT/O21cKzPrGb+KSfCUReer47Am qHOw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:cc:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding; bh=p6fXN/zS/zND2SpdY9qTubGL39E++nU1YObZB7P105c=; b=XpGcHTz8bprGcCsLXA5km7Ifi8ahhDiudgH2ZL5UueQaNYLp23o9OD9GYqbOw9cV/j oMfuM1pnYHjW5GIeQwPDlFNshvY7NxKsYgaeGJZYcKM3eTXx6ysqxKorgJHeOqbqltYa KlI5dDOwSNWwHQ43CJXH+ZJu0YK7zR/mwt7fB8VKMWtE7Fuw/PMxWrI6TaGI+mDHwJlV WUGOlCFV4Sq+gWodF6UaHqK+5ZSFYimDjZQIi9IWNjz/N7BN1UKDGOPYezCXkKY+kKtT 1d5O7F86IXHokn3V7YHPJioHsJdr/T1UVokO2UtaE/EY/x31TmLdk5+B8Q/pn1Bj9iYc wEJw== X-Gm-Message-State: APjAAAUFmYVGSPQsYEomcmBbsN3QfGt8aF79BQHaD+3N+c8V6UG6Ss4m V2SUGS2VCf+hkwQVSKNDcA344yW9 X-Google-Smtp-Source: APXvYqxXu924vXuBkXrwgTTVl7dniQe4re2mbttw3eCNEYRmX7X56IZkPPHy72YvocjFuCctY2f0SA== X-Received: by 2002:ad4:4949:: with SMTP id o9mr8916596qvy.189.1575575455871; Thu, 05 Dec 2019 11:50:55 -0800 (PST) Original-Received: from ?IPv6:2603:400a:0:82c:fff1:4e82:4e43:cc9e? ([2603:400a:0:82c:fff1:4e82:4e43:cc9e]) by smtp.googlemail.com with ESMTPSA id l7sm5758058qtf.84.2019.12.05.11.50.55 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 05 Dec 2019 11:50:55 -0800 (PST) In-Reply-To: <83a786iyvc.fsf@gnu.org> Content-Language: en-GB X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: bug-gnu-emacs@gnu.org List-Id: "Bug reports for GNU Emacs, the Swiss army knife of text editors" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-gnu-emacs-bounces+geb-bug-gnu-emacs=m.gmane.org@gnu.org Original-Sender: "bug-gnu-emacs" Xref: news.gmane.org gmane.emacs.bugs:172930 Archived-At: On 2019-12-05 10:19, Eli Zaretskii wrote: >> Cc: casouri@gmail.com, 38485@debbugs.gnu.org >> From: Clément Pit-Claudel >> 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 :/