coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicode tokens?

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Unicode tokens?
Date: Thu, 9 Mar 2017 11:13:21 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f173.google.com
Ironport-phdr: 9a23:wyCUfhBcoqPRes/kZ9V5UyQJP3N1i/DPJgcQr6AfoPdwSPT9ocbcNUDSrc9gkEXOFd2CrakV1qyK7euwAyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5Yb5+Nhq7oATeusQVn4dpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9RtgqxFrhKvpx9xzYDab46aNvVxYqzTcMgGRWdCRMtdSzBND42+YoYJEuEPPfxYr474p1YWsxa+AROrBObxxT9Omn/5xbc00+U9EQ3fwgEgG8gBsGnJo9rrMKcZTOe4w7XQzTXCc/NZxTP955LVch88v/6MWal9ccXUyUY1FgPFik+cppDiPzOQz+kAtXWQ4eRnVeKqkWEnqgdxryCgxsctlonJhp8VxUve+Splx4Y1IMW0SEF9Yd65CpdQsDuaN4RwT8g/QG9ooD43xqMatZO/ZiQHy5QqywTBZ/CZb4SE+A/vWeSfLDtgmn5pZK6ziwu3/EWvyODwSsy53VVRoSZbj9bBs20B2AbW58WDUfRy5Fyu1DOT2AzO6OxJI0U5mKjVJpE63LI9k4QfvVjZESLynkj9kbWYeV8++uey7uTqerXmqYGYN49zkgz+N74hms27AeghKwgOXHSX9f2y1LH+/0D0Tq9GjvIxkqnev5DaIdoUqrSlDA9S14Yv8xe/DzG439QEhXQLMk5JdRadg4XqO1zCOu70Aemjj1i2jTtmxf7LMqXkAprXL3jDlLnhfax6605Z0Ac80chf55NICr4dJPL8QFLxu8HGAR89KAG0zOPnB8981oMaQ26AHqiZMKbKvV+S+u0vO/WMZJMSuDvlN/cl4OfugWYlll8ZYKmmxoAaaGu4H/RjO0WWe2DggtYHEWcQvwoxVvbmiFOYUW0bW3HnVKUlozo/FYiODIHZR4nrjqbS8j28G8h9YuFDB1aQJk/pa8CvX/4RZC+Waptqij0YXryoVoMs0TmhsQb7z/xsKe+CqX5Qjo7qyNUgv76brho17zEhV8k=

On 2017-03-09 10:24, Matej Kosik wrote:
> On 03/08/2017 11:53 PM, Clément Pit-Claudel wrote:
>> On 2017-03-08 15:36, Matej Kosik wrote:
>>> (I jumped to the conclusion that this is because of some Emacs
>>> specific fonts because I've seen this behavior only in Emacs, nowhere
>>> else).
>>
>> This is due to Emacs respecting the incorrect metrics of certain TeX fonts
>> (other applications typically ignore them);
>> see https://github.com/cpitclaudel/company-coq/issues/15 and
>> https://lists.gnu.org/archive/html/bug-gnu-emacs/2015-05/msg00696.html for
>> more details.
>
> I've never seen such a behavior in TeX.

That isn't surprising; see the bug-gnu-emacs thread for details (long story
short: Tex Live ships copies of Latin Modern and other fonts that specify
incorrect metrics; XeTeX rendering isn't affected, because it doesn't use
these metrics).

Re: [Coq-Club] Unicode tokens?, (continued)