The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

The bug is fixed in github now.

The question remains to decide if we keep this feature in pg.

The main advantage of this feature is that you keep non-unicode text
in your files. Still today it seems to be an advantage. I don't
understand exactly why because now all editors support unicode. But
people still fear unicode.

The main disadvantage of this feature is that it introduces
inconsistencies between view modes of a file: the length of lines is
not the same with or without the tokens hence the layout of your files
is ugly in either one or the other mode.

I tend to use unicode when I work alone, and stick to ascii/latin when
working with others. In these cases I kind of like unicode tokens. But
going for company-coq pretty-printing is straightforward.

P.

2017-03-07 16:48 GMT+01:00 Paul A. Steckler 
<steck AT stecksoft.com>:
> 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