coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicode tokens?

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: Tom Hirschowitz <tom.hirschowitz AT univ-smb.fr>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Unicode tokens?
Date: Tue, 7 Mar 2017 10:48:39 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f174.google.com
Ironport-phdr: 9a23:nuCnBx9jJZPX1P9uRHKM819IXTAuvvDOBiVQ1KB91uwcTK2v8tzYMVDF4r011RmSDNidt6gP27Ge8/i5HzdfsdDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJdb974EY/Kjsmxy/v6u9iKO10J13KBZuZOKxD+jQTLrcIWhpRjNrR5ngfOpz1Iev5NzmNvOlOPjT7h4MauuYVm+WJeoaRlv8VHSODxe7kyBehTCy1jOGQo7uXqswPCRE2B/C1PfH8Rl08COwHY6FnTGN/Kribxte5wwmPSadbqQLs3cS++4qxoUxjmlGEMMDtvozKfsdB5kK8O+EHpnBd42YOBJdjNbPc=

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

[Coq-Club] Unicode tokens?, Paul A. Steckler, 03/06/2017
- Re: [Coq-Club] Unicode tokens?, Makarius, 03/06/2017
  - Re: [Coq-Club] Unicode tokens?, Théo Zimmermann, 03/06/2017
    - Re: [Coq-Club] Unicode tokens?, Clément Pit-Claudel, 03/06/2017
      - Re: [Coq-Club] Unicode tokens?, Christian Doczkal, 03/07/2017
        
        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
- 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