coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicode tokens?

From: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Unicode tokens?
Date: Tue, 7 Mar 2017 15:56:33 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christian.doczkal AT ens-lyon.fr; spf=Pass smtp.mailfrom=christian.doczkal AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:YnIB2BPse3JS2g0QeF0l6mtUPXoX/o7sNwtQ0KIMzox0Iv7/rarrMEGX3/hxlliBBdydsKMZzbaM+P+5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT69bL9oIxi6swrdu8sLjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaktF+grxVoByhpBJxzYDbb46XO/Vica3QZs8aSGlbU8pNSyBMDIGxYo0SBOQBJ+ZYqIz9qkMQoBu+HwmsBfjvyiNJhnDs260xzuovEQba0w0hHNIBqnDUp8jyOagOUeC11qjIzS7fb/NXwzj97pLEfQ0mof6QXLNwctDeyU00GgzbiFWQspXpPzeV1+QKtWiX9eRgVfi2hmMhtgp/rD+vxsI2hYnIgIIY0l/E9SRlwIY1ON23U1R3bsKjEJtVsSyRKoh4Qts6Tm11tys21qcKtJy5cSQQ1ZgqxhzSZ+aZf4SW/B7vTPudLDhkiH5/er+yhQy+/VWux+HmSMW4zktGoyxYmdfWrH8NzQbc6s2fR/t94Eih3TGP2hjX6u5eOk87jrTUJ4Q/zb42jZofqEDDHy/xmEXwlqOWeF8k9vCp6+ThfLrmuoeRO5J7hw3iKKgjmM6yDf4lPgUPXWWX4/qw2KP98UHhRbVFlPw2kq3XsJDAIsQbo7a0DBNV0oY56ha/FCum0NUCknkBNl5KZRWHgJToOlHNOv/4CeyyjEqqkDdw3vzGOr3gApLLLnTZnrfhZ65x61RAxwor0dBf+5VUB6kdL/L0Q0/9rcDXDhskMwOv2OvnE9V81oYGWW2VGKOZMaXSsUWJ5u01OeWMapUV637BLK0u4Oerhnskk3cce7Oo1N0ZciOWBPNjdm6Ze3v3ntYIFy8muQEsT+XuwAmJUSRSfGqzVqR66jYwGoGvCa/OQJvohK2G2mG1BMsFNSh9FlmQHCKwJM2/UPAWZXfKLw==

Hello,

On 07/03/17 15:33, Benjamin C. Pierce wrote:
> 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.

The setup I (and my former colleagues) use nowadays is to use
Company-Coq's prettify-symbols mechanism to view/edit plain ASCII files
and then use CoqDocJS[1] to generate HTML that displays as Unicode but
copies/pastes as ASCII.

Not sure how CoqIDE fits into this though (or what font issues one might
encounter across different operating systems).

Best,
Christian

[1]https://github.com/tebbi/coqdocjs

[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