--- a/Admin/page/main-content/faq.content Fri Apr 22 02:09:10 2005 +0200
+++ b/Admin/page/main-content/faq.content Fri Apr 22 04:12:24 2005 +0200
@@ -209,6 +209,39 @@
<h2>Interface</h2>
+ <table class="question" width="100%"><tr><td>ProofGeneral appears to hang when Isabelle is started.</td></tr></table>
+
+ <table class="answer" width="100%"><tr>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse 9.0/9.1
+ <p>
+ 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.
+ <p>
+ 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:
+ <p>
+ <tt>$ LC_CTYPE=en_GB Isabelle &</tt>
+ <p>
+ 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 <tt>LANG</tt>.
+ <p>
+ 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 ]
+ <p>
+ 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.<td></td></tr></table>
+
<table class="question" width="100%"><tr><td>X-Symbol doesn't seem to work. What can I
do?</td></tr></table>