Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq 8.10.0

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.10.0


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Coq 8.10.0
  • Date: Thu, 10 Oct 2019 10:05:10 +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-f68.google.com
  • Ironport-phdr: 9a23:ayYeDRez5p+p3fKTpQ2iSkX6lGMj4u6mDksu8pMizoh2WeGdxcS+ZR7h7PlgxGXEQZ/co6odzbaP6Oa+AydZus7JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/Qu8UIjoduN6g8xgfUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMDYShYYsSFOoBJfhXoJXhp1UAqhu+ABOjBOLpyjRVgnP70qk33+EnHArb3gIvAsgOvWzbo9X7NqgcUe67wqrVwzvdc/xY1izw6JTRch07vf2AQa58fMjXxEIyFw3FlFKQqYn9Mj2L1uQKqW+b4PJjWuKujm4nrh9+oiKqxsg2jInJgJ8ex1fY9SV53ok1Ise0SU96Yd6hFZtQtjqXN4RzQsw4QmFovDw2xaEBuZ6+ZSUHzoksyRDYa/yCaYeI4xTjWf6UITd/g3Jlf6iziAq18UilzOD3S8q60E5SoyZbjtXBsmoB2h/T58SdVPdx40Ws1SyO2g3Q7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2ibWZdkQg+uSx9eTneajqqoaSN4J1iQzyKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqkqTBrpzWOcAWqrS6DgJVyIov9QuzAjW83NkZnnQLNFdFdwiGj4jtNVHOOvf4DfKnjlSwkDdk2ffGMqfgA5XMK3jDlbbhcK1y605Z0gUzzNRf64hIBbEGJfL/QlXxu8DADh8lLwy0xP7qB8l61oMHQG6AHquZML7JvlKT/eIuI+yMZJcPtzrnKvgl4eTujX4jllMHc6mpx8hfVHftNfN/a26dfHCk1twGCCIBuhc0ZO3sklyLFzBJMSWcRaU5sw07iYWRP4bGQ423hbWH2m/vAp1bYSZUC1WJEF/ncoyFX7EHbyfEcZwpqSANSbX0E9xp7hqprgKvjuc+d7eGymgjrZvmkeNNyajTmBU1r2EmCs2c1ySTVDgxkD1YATAx2697rAp2zVLRifEp0cwdLsRa4rZyail/MJfdy+JgDNWrA1DOe96ITBCtRdD0WGhtHOJ0+McHZgNGI/vnlgrKhnP4DLoclrjND5sxoPrR

Hi Ian,

There is no reason why it shouldn't. I don't think that any of the
keybindings within CoqIDE would override the ones defined at the level
of the window manager. For instance, on my machine Shift+space is
already bound to insert a non-breaking space, and it continues to be
like that in CoqIDE (and thus the Unicode input keybinding is not
available). Moreover, every CoqIDE keybinding is configurable so you
can change it to whatever suits you best.

This feature is rather meant to all the people for whom configuring
XCompose or something similar would be too much of a hassle.

Théo

Le mer. 9 oct. 2019 à 22:13, Ian Zimmerman
<itz AT very.loosely.org>
a écrit :
>
> On 2019-10-09 15:27, Vincent Laporte wrote:
>
> > The 8.10.0 release of Coq is available.
>
> > - easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.
>
> It is reasonably easy for me now (coq 8.9) on Linux with XWindow, using
> the XCompose mechanism. I would much rather continue doing it this way
> (rather than some new special CoqIDE way), because it generalizes to all
> other XWindow programs, and even (with some extra configuration) to
> console programs. So, I have to ask, will the new CoqIDE work with
> XCompose? I think it should, because my Emacs does, and it's built with
> gtk3. But I want to be reassured before switching.
>
> Thanks for coq, an amazing project.
>
> --
> Please don't Cc: me privately on mailing lists and Usenet,
> if you also post the followup to the list or newsgroup.
> To reply privately _only_ on Usenet and on broken lists
> which rewrite From, fetch the TXT record for no-use.mooo.com.



Archive powered by MHonArc 2.6.18.

Top of Page