Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Unicode tokens?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicode tokens?


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Unicode tokens?
  • Date: Wed, 08 Mar 2017 10:59:59 +0000
  • 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-qk0-f182.google.com
  • Ironport-phdr: 9a23:XAiW6RFarKlicANFLHVH1Z1GYnF86YWxBRYc798ds5kLTJ76oMiwAkXT6L1XgUPTWs2DsrQf2reQ7/yrADNIoc7Y9itdINoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScaBx/iwguu14tjYZxhCrDu7e7J7ahus/ivLscxDvYvjLZEDyx7Mr2FNcuJQjTd0JV+U2QT948Kx1JFm+iVU/fkm8pgTAu3BY60kQOkAX3wdOGcv6ZizuA==

Company-Coq prettification has some default settings, which do not include delta or any other Greek variable as far as I am aware, but it is easy to extend, in your personal settings, or by an option in the file using these extensions.


Le mer. 8 mars 2017 11:15, Tom Hirschowitz <tom.hirschowitz AT univ-smb.fr> a écrit :

Aha, right, I've already encountered this one, but had forgotten.

Apparently, company-coq isn't much better: it displays something like
delta₁.

Good luck!
Tom

"Paul A. Steckler" <steck AT stecksoft.com> writes:

> On Tue, Mar 7, 2017 at 5:43 AM, Tom Hirschowitz
> <tom.hirschowitz AT univ-smb.fr> wrote:
>> What kind of bugs are you thinking of?
>
> For example, in the PG file coq/example-tokens.v, there is the text
> "delta__1", which should show a subscripted Greek letter. Instead, the
> text appears verbatim.
>
> I think I've tracked down this bug to the regular _expression_ that's
> generated for token matching.
>
> -- Paul



Archive powered by MHonArc 2.6.18.

Top of Page