coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vadim Zaliva <vzaliva AT cmu.edu>
- To: coq-club AT inria.fr
- Cc: Tom Hirschowitz <tom.hirschowitz AT univ-smb.fr>
- Subject: Re: [Coq-Club] Unicode tokens?
- Date: Wed, 8 Mar 2017 09:32:34 -0800
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wr0-f180.google.com
- Ironport-phdr: 9a23:9xe+2h0bvQJPICJIsmDT+DRfVm0co7zxezQtwd8Zse0SKPad9pjvdHbS+e9qxAeQG96KtrQY16GH4ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhDexe7x/IRq5oQjVssQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LpwRRT2lCkIKSI28GDPisxxkq1bpg6hpwdiyILQeY2ZKeZycr/Ycd4cWGFPXNteVzZZD4y+YYsBD+QPM+VFoYfju1QDtgGxCRW2Ce711jNEmn370Ksn2OohCwHG2wkgEsoBv3vOsdr1NaISWv22w6bSyTXDbu1W1i3g44XPbBAgoOuDXbZxccrP00YiDB/KjlCNqYD/ITyay/kNvnGd4uF9Vuyvk3Yqpx9trjWr3MshiYnEipgIxlza9ih12ps5KN6kREN9fNWqCoFftzuAOItzWs4iQ39nuCI9yrAevJ60ZikKyJA+yx/RcfyLb5GE4hz+WOuSPTt0nn1leLW4hxa99Uiv1PfwWdWz0FZPtiZFk9/MuW4R1xHL9MSLVv9w8l2i1DuPzQzf9/9ILEMumabGKJMt3qY8lp8JvkTCGi/2ll/2jKiTdkg85Oin8fnoYrTjppOGNo57kAX+MqUwmsOlGuk5PBYBX3OH+eimyLLj+FD5TK9UgfIrj6nVqIraKtgDpq6lHw9V1Z4u5Aq4Dze/ydgXgX0HLE9edx+clIjoO1TOIOjiAvulglSsli1rx/HcMbH7DJXNNCuLrLC0drFkrkVY1QAbzNZF5psSBKtSDuj0XxrPvdDZC1cLOgi13e+vXMtv34cfR2unCaqEdq7erAnbtaoUP+CQadpN637GIP8/6qur1CdhlA==
One problem with Unicode is working with files outside Emacs. For example, if my source files use greek letter delta as Unicode character it makes it difficult to use command-line tools like grep or "/" command in "more" in the lack of emacs Unicode input facilities. This is the reason I prefer to save .v files as ASCII, but I really love Unicode rendering in emacs.
--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
On Wed, Mar 8, 2017 at 8:34 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:
The bug is fixed in github now.
The question remains to decide if we keep this feature in pg.
The main advantage of this feature is that you keep non-unicode text
in your files. Still today it seems to be an advantage. I don't
understand exactly why because now all editors support unicode. But
people still fear unicode.
The main disadvantage of this feature is that it introduces
inconsistencies between view modes of a file: the length of lines is
not the same with or without the tokens hence the layout of your files
is ugly in either one or the other mode.
I tend to use unicode when I work alone, and stick to ascii/latin when
working with others. In these cases I kind of like unicode tokens. But
going for company-coq pretty-printing is straightforward.
P.
2017-03-07 16:48 GMT+01:00 Paul A. Steckler <steck AT stecksoft.com>:
> On Tue, Mar 7, 2017 at 5:43 AM, Tom Hirschowitz
> <tom.hirschowitz AT univ-smb.fr> wrote:
>> What kind of bugs are you thinking of?
>
> For example, in the PG file coq/example-tokens.v, there is the text
> "delta__1", which should show a subscripted Greek letter. Instead, the
> text appears verbatim.
>
> I think I've tracked down this bug to the regular _expression_ that's
> generated for token matching.
>
> -- Paul
- Re: [Coq-Club] Unicode tokens?, (continued)
- Re: [Coq-Club] Unicode tokens?, Théo Zimmermann, 03/07/2017
- Re: [Coq-Club] Unicode tokens?, Paul A. Steckler, 03/06/2017
- Re: [Coq-Club] Unicode tokens?, Benjamin C. Pierce, 03/07/2017
- Re: [Coq-Club] Unicode tokens?, Christian Doczkal, 03/07/2017
- Re: [Coq-Club] Unicode tokens?, Benjamin C. Pierce, 03/07/2017
- Message not available
- Re: [Coq-Club] Unicode tokens?, Paul A. Steckler, 03/07/2017
- Re: [Coq-Club] Unicode tokens?, Tom Hirschowitz, 03/07/2017
- Re: [Coq-Club] Unicode tokens?, Théo Zimmermann, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Clément Pit-Claudel, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Tom Hirschowitz, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Pierre Courtieu, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Vadim Zaliva, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Matej Kosik, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Vadim Zaliva, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Paul A. Steckler, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Makarius, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Clément Pit-Claudel, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Matej Kosik, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Clément Pit-Claudel, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Matej Kosik, 03/09/2017
- Re: [Coq-Club] Unicode tokens?, Clément Pit-Claudel, 03/09/2017
- Re: [Coq-Club] Unicode tokens?, Matej Kosik, 03/09/2017
- Re: [Coq-Club] Unicode tokens?, Matej Kosik, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Vadim Zaliva, 03/08/2017
- Re: [Coq-Club] Unicode tokens?, Tom Hirschowitz, 03/07/2017
- Re: [Coq-Club] Unicode tokens?, Paul A. Steckler, 03/07/2017
Archive powered by MHonArc 2.6.18.