This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse 9.0/9.1
+
+ RedHat 8 and later has glibc 2.2 and UTF8 encoded output may be
+ turned on in default locale. Unfortunately Proof General relies on
+ 8-bit characters which are UTF8 prefixes in the output of proof
+ assistants (inc Coq, Isabelle). These prefix characters are not
+ flushed to stdout individually. As a workaround we must find a way
+ to disable interpretation of UTF8 in the C libraries that Coq and
+ friends use.
+
+ Doing this inside PG/Emacs seems tricky; locale settings are
+ set/inherited in strange ways. One solution is to run the Emacs
+ process itself with an altered locale setting, for example,
+ starting XEmacs by typing:
+
+ $ LC_CTYPE=en_GB Isabelle &
+
+ The supplied proofgeneral script makes this setting if it sees
+ the string UTF in the current value of LC_CTYPE. Depending on your
+ distribution, this variable might also be called LANG.
+
+ Alternatively you can set LC_CTYPE or LANG inside a file ~/.i18n, which will
+ be read by the shell. This will affect all applications, though.
+ [ suggestions for a better workaround inside Emacs would be welcome ]
+
+ NB: a related issue is warnings from x-symbol: "Emacs language
+ environment and system locale specify different encoding, I'll
+ assume `iso-8859-1'". This warning appears to be mainly harmless.
+ Notice that the variable `buffer-file-coding-system' may determine
+ the format that files are saved in.
|