coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicode tokens?

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr, Coqdev <coqdev AT inria.fr>
Subject: Re: [Coq-Club] Unicode tokens?
Date: Mon, 06 Mar 2017 20:29:03 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f172.google.com
Ironport-phdr: 9a23:qa3l8R36qPTAlmM8smDT+DRfVm0co7zxezQtwd8ZseIWLvad9pjvdHbS+e9qxAeQG96KtrQY06GP6P+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDqwbal9IRmqogndq8cbjIl/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6xbrxChqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4TzuVsOqgG5BQa0B+zvyzpIhnro0q0g1uQuCwfG3Ao9FN8JrHTUrMv6NKAIXeG0zanIyDDDb/JN1Dfy7YjHaBEhofWWUb1sdsrRzFAiGgXYhVuTsYzoJy2Z2vgJvmSB7OdtVfijh3A5pw1tuDSj28UhhpfPi4kI0F7L7z95z5wwJdCgSE50f9qkEJxIuiGfLYR2Q8ciT3hxuCY51rEKoJC7cDUIxZg53RLfZPuHc4+H4hLnSumdOyt3hHVgeL6nhhay91avyvHkW8WqzFpHqjBJn9rMu3wXyRDf9NSLRuFg8kqjxzqDzwXT5ftFIUAwm6rbMZkhwrsom5oPsUTMACj2lF/3ja+Xc0Uk/+mo5v/oYrXjvJCcNot0hhviPaQpn8yzGf44PRQWX2iH5eS806Xu8lH+QLVTl/E5jq3ZsI3BKskAva64AwpV0p455BqlDjem1s4YnXgdI15fdhKHlZDjO0vSL/DgEfe/n1OsnS93yPDBJ73uH4vCLmbYnbf6fbd97lZcxxApwdBe4ZJUELABL+jpVk//rtyLRiM+Zgez2qPsDMh3/oIYQ2OGRKGDdOv5tkaE6/xnd+KLfYMYph78LeIk7rjglylqt0UaePyV3RoQX0K5G/FrOUCQZ3yk1ssBHGBMrAs7Se3Ch1iLUDoVbHG3CfFvrgonAZ6rWN+QDrumh6aMiX+2

That's another feature which is also provided by Company-Coq (advertised as prettification), right?

Le lun. 6 mars 2017 21:18, Makarius <makarius AT sketis.net> a écrit :

On 06/03/17 21:10, Paul A. Steckler wrote:
> Is anyone using the "Unicode tokens" feature of Proof General?
>
> That's the feature that turns certain keywords and symbols, like
> "forall", into pretty Unicode versions.
>
> That feature has some bugs right now, so it would be nice to know if
> there are users who would appreciate fixes.

Many years ago, it was used by Isabelle Proof General, but Isabelle no
longer supports Proof General since October 2014.

I am unsure if it was ever relevant for Coq Proof General.

Makarius

[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