diff options
Diffstat (limited to 'FAQ')
| -rw-r--r-- | FAQ | 34 |
1 files changed, 30 insertions, 4 deletions
@@ -5,6 +5,33 @@ For latest version, see http://www.proofgeneral.org/FAQ Credits to the anonymous authors of questions/answers below. +Please also check the BUGS file. + +----------------------------------------------------------------- + +Q. Emacs appears to hang when the prover process is started. + +A. This may be because of UTF-8 issues e.g in Red Hat 8.0/9/glibc 2.2 + +RedHat 8 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 in a different locale, for example, starting XEmacs by +typing: + + $ LANG=en_GB xemacs & + +Another solution is to set LANG inside a file ~/.i18n, which will +be read the shell. This will affect all applications, though. +[ suggestions for a better workaround inside Emacs would be welcome ] + + ----------------------------------------------------------------- Q. XEmacs 21.4 displays a progress bar during fontification which @@ -139,11 +166,10 @@ A. These are part of the 8 bit character codes used by X Symbol to To fix, type - M-x font-lock-fontify-buffer + M-x x-symbol-decode-recorde - or M-x x-symbol-fontify. If that doesn't work, type M-x - font-lock-mode twice to turn font-lock off then on. - Or reload the file. + If that doesn't work, type M-x font-lock-mode twice to turn font-lock + off then on. Or reload the file. Note that X-Symbol is more robust when used with XEmacs/Mule. |