coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq and Unicode

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Coq and Unicode
Date: Sat, 3 Aug 2019 15:50:35 +0200
Authentication-results: mail2-smtp-roc.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-vs1-f50.google.com
Ironport-phdr: 9a23:qOMv+BD8XpNEVAX7w1ZYUyQJP3N1i/DPJgcQr6AfoPdwSPT+rsbcNUDSrc9gkEXOFd2Cra4d0ayP6/mrBzxIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK1+IA+roQnNq8UajopvJ6UswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKLCAy/n3JhcNsjaJbuBOhqAJ5w47Ie4GeKf5ycrrAcd8GWWZNW8BcWCtcDIOhdIsPF/QOMvpEr4fzoFsOqAGxBQiqBOjyzjNFiXv70ag83u88Ew/JwRYgEsoBv3Tartr7NKkcX+OowqfW0TrOdOlZ1Svn5YXSbhwtvfOBULRtesTR00kvEAbFg02Op4zlJTSV0fwCvGua7+plUOKglXQnqwRrrTipwMcnl47Ehp4Vyl/a8iV12oc0Jdy9SE5+YN6pC5RQtySAOIt3RsMuWX1nuCE/yrAfv5OwYSYEyJMixxHFavyHdZCF4h3iVOaNITd4mWlqdKi+hxa16USgy+v8VtWq31ZOtCZKj8fDu3YQ3BLQ8siKUuVx8lul1DqV1A3e6vtILV4pmafZMZIswqI8m5wOukrZBCD2gl/5jKqOe0Uk5Oeo7+Pnb63jppCGNo90jhjyMro1msCiGOg4PAgDU3SB9eSz073j+kL5QLFUgfEsjqbZt5XaKdwapq6/HQBVzp4u5wijAzqiytgVnnkKIEhbdB6ajYXlIVHDLOzgAfe6mVuskTNrx/7cPr3mB5XANmTDkLf/crZ68UJdyQszzdVa55JVEbwBL/fzVVXwtNzcFBM2Lwu0w+P/BNVnyoweQX6PArOeMK7KrVCI4fsvL/CQa48RpTbyMOMo5+XujH88gV8SZ7Ol3ZoRaHCiH/RpOV+VYXT2goRJLWBflQ0nBMfulVfKBTVUfjO5W782zjA9EoOvS4nZENODmruEiRu7n5phVGFDD12WFH7ucc3QR/cBb2SAI8pkkxQLULGgT8kq0hT451yy8KZuMueBon5QjpnkztUgorCKzExgxXlPF82Yllq1YSR0k2cPHWJk2al+pQlj0Q7G3/UgxfNfEtNX6rVCVQJobceAndw/MMj7X0f6RvnMUEyvG4z0DjQ4T9Z3yNgLMR4kSoeSyyvb1i/vOIc70rmCBZg66KXZhiGjKMN0ynKA364k3QAr

Hi Michael,

My own testing on Linux was not conclusive because Shift+space is already bound on my machine to insert non-breaking spaces. But I successfully used the menu instead of the keyboard shortcut.

Best regards,

Théo

Le sam. 3 août 2019 à 09:46, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Hi Theo,

> The situation has become better in CoqIDE "out of the box" in version
> 8.10 thanks to the effort by Arthur Charguéraud. See the documentation
> here: https://coq.github.io/doc/V8.10+beta2/refman/practical-
> tools/coqide.html#coqide-unicode

I just tested in on Windows on a fairly recent 8.10 build and Shift+Space simply inserts a space here. Can you confirm that it works on Linux on 8.10?

The chosen font would support Unicode.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

Re: [Coq-Club] Coq and Unicode, Benjamin C. Pierce, 08/02/2019
- <Possible follow-up(s)>
- RE: [Coq-Club] Coq and Unicode, Soegtrop, Michael, 08/03/2019
  - Re: [Coq-Club] Coq and Unicode, Théo Zimmermann, 08/03/2019