Re: [isabelle] x-symbols and AFS?

On Thu, 1 Jul 2010, 许庆国 wrote:

When I start   Isabelle2009-2 In XEmacs 21.4 under cygwin 1.7 , the following warning and error messages show.

(1) (x-symbol/error) Couldn't add /usr/local/Isabelle2009-2/contrib/ProofGeneral/x-symbol/etc/pcf/ to X font path
(2) (x-symbol/error) Couldn't add /usr/local/Isabelle2009-2/contrib/ProofGeneral/x-symbol/etc/pcf/ to X font path

But the Isabelle 2009-1 works fine.

In principle there should be no difference of Isabelle2009-1 vs. Isabelle2009-2 here -- at least in the standard distribution bundles, which contain exactly the same version of ProofGeneral-

According to the following mail,  I have tried sereval methods:
1)      xset fp+ tcp/
   gives the following errors message:
   xset:  bad font path element (#23), possible causes are:
   Directory does not exist or has wrong permissions
   Directory missing fonts.dir
   Incorrect font server address or syntax

This used to work until a few months ago -- either our font service is broken, or there have been some protocol changes in that the server does not understand. Since X-Symbol and X11 fonts are being phased out eventually, it is not worth investing too much time on it.

   2 [main] xemacs-21.4.22 2960 exception::handle: Exception: STATUS_ACCESS_VIOLATION
   805 [main] xemacs-21.4.22 2960 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
     2 [main] xemacs-21.4.22 200 exception::handle: Exception: STATUS_ACCESS_VIOLATION
   636 [main] xemacs-21.4.22 200 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
     2 [main] xemacs-21.4.22 3852 exception::handle: Exception: STATUS_ACCESS_VIOLATION
   643 [main] xemacs-21.4.22 3852 open_stackdumpfile: Dumping stack trace to xemacs-21.4.22.exe.stackdump
     2 [main] xemacs-21.4.22 788 exception::handle: Exception: STATUS_ACCESS_VIOLATION

I've also seen such generic xemacs crashes on cygwin Cccasionally. My guess is that this is due to the general situation of xemacs being old and unmaintained for a couple of years.

The reason why ancient xemacs is needed on Cygwin is the lack of GNU Emacs 22 on that platform. ProofGeneral-3.7.x does not work with the newer GNU Emacs 23 line, which is generally far superior.

Anyway, the Proof General 4.x code base has again become quite usable, so you can also try the CVS version from together with GNU Emacs 23 on Cygwin.

Since there is no X-Symbol mode in that version, you can't get any problems with it :-) You will need a good Unicode font with math symbols, though. Isabelle2009-2/lib/fonts/IsabelleText.ttf can be installed manually on Windows and then configured as default font inside Emacs. That's not perfect, but much better than anything we've ever had so far.

Maybe David Aspinall can provide a proper development snapshot of the current Proof General CVS.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.