coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicode tokens?

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr
Cc: Coqdev <coqdev AT inria.fr>
Subject: Re: [Coq-Club] Unicode tokens?
Date: Tue, 7 Mar 2017 09:33:04 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT hound.seas.upenn.edu
Ironport-phdr: 9a23:zzT2iBZDQMlrp2dv6jzRgWb/LSx+4OfEezUN459isYplN5qZpsW/bnLW6fgltlLVR4KTs6sC0LuL9fy6EjJQqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2auejsh7v3o8ebI1oQxWn1XbQnJxKv6A7Vq8M+gI14K693xAGajGFPfrEc725uJ1uWnhC0zYH4xJ9u6S9d8bp1/cVYUKjgdKkQRr1DSik+PmYzosDnqE+QHkO0+nIAXzBOwVJzCA/f4USlBpo=

> There are some definitions in the Coq part of PG for syntax
> highlighting for Software Foundations, that uses the Unicode tokens
> mechanism. Also, there is a test file in the Coq part of PG for
> Unicode tokens.

Since SF has been mentioned, let me add that I have never been satisfied with
our handling of special symbols. If someone offers a good alternative (i.e.,
one that works well with both CoqIDE and PG, can be used to generate pretty
HTML, and doesn’t require naive users to fiddle with their system font
configuration) I’ll jump on it.

- Benjamin

[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