The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi Vadim,

On 03/08/2017 06:32 PM, Vadim Zaliva wrote:
> One problem with Unicode is working with files outside Emacs. For example, 
> if my source files use greek letter delta as Unicode character it makes it 
> difficult to use command-line tools like grep or
> "/" command in "more" in the lack of emacs Unicode input facilities.

I guess that it is not the responsibility of the "grep" and friends to enable 
you to type unicode characters.
(it is the job of programs providing "input method", I guess, such as "xim", 
"uim" and many others).

I guess that few people bother using Unicode glyphs because Emacs ships 
broken fonts.

> This is the reason I prefer to save .v files as ASCII, but I really love 
> Unicode rendering in emacs.
> 
> 
> 
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060
> 
> 
> On Wed, Mar 8, 2017 at 8:34 AM, Pierre Courtieu 
> <pierre.courtieu AT gmail.com
>  
> <mailto:pierre.courtieu AT gmail.com>>
>  wrote:
> 
>     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
>  
> <mailto:steck AT stecksoft.com>>:
>     > On Tue, Mar 7, 2017 at 5:43 AM, Tom Hirschowitz
>     > 
> <tom.hirschowitz AT univ-smb.fr
>  
> <mailto: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
> 
>