On 30/09/10 8:20 AM, [email protected] wrote:
> Hi
> I am having difficulty in getting the pretty-printer to work properly
> in a recent installation of HOL4K6 on my sun workstation with Solaris
> 10. Quantifiers and operators are not displayed properly by the
> pretty-printer (both in xterm and inside Emacs). [...]
> I have also tried installing/compiling HOL4K6 on PCs with windows
> (vista, windows7) and Linux (SUSE) operating systems and experience
> the same problem with the pretty-printer. Everything seems okay on
> cygwin though, that is, it works exactly as its described in "Release
> Notes -> New features". I am very sure that I have followed the
> instruction for building HOL from sources exactly and am wondering
> what can I do to get the pretty-printer to display information
> correctly?
You have two options:
* have your terminals/emacs set up to handle UTF8 output
* turn Unicode off (set_trace "Unicode" 0).
For a standard Unix sort of setup, setting the LANG environment variable
to something with a .UTF8 suffix should get xterms and the like
(gnome-terminal, for example) doing the right thing. You will also have
to ensure that your fonts are good enough.
For example, in my relevant bash config file, I have
declare -x LANG=en_AU.UTF8
For emacs, I recommend the following
(set-selection-coding-system 'utf-8)
(set-next-selection-coding-system 'utf-8)
(setq process-coding-system-alist '((".*" . utf-8)))
I'm glad to hear that the output looks good on Cygwin. On vanilla
Windows, I don't know how to get good console output. Emacs on Windows
works well though.
Michael.
------------------------------------------------------------------------------
Start uncovering the many advantages of virtual appliances
and start using them to simplify application deployment and
accelerate your shift to cloud computing.
http://p.sf.net/sfu/novell-sfdev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
