Re: [isabelle] Isabelle2008



On Mon, 13 Jul 2009, John Matthews wrote:

Unfortunately I'm stuck with xemacs at the moment, as Isabelle2008 is part of a larger toolchain (not written at Galois) that depends on xemacs. I'm letting them know that Isabelle is phasing out support for that, but it will take them a while.

This is really just a matter of Proof General, not Isabelle. If there will ever be a version of PG 4.0, it will be for GNU Emacs only. (David Aspinall has announced that more than 1 year ago, IIRC.)


In the meantime, I'd like to be able to copy subgoals from the xemacs proof buffer back into my theories. Unfortunately the xsymbols don't get copied correctly. For example, the proof term:

\<forall>x. x \<le> (3\<Colon>'a)

gets pasted as:

~x. x ~ (3~'a)

And the xsymbols menu disappears when I select the proof buffer, so I can't even use that.

Any suggestions?

This looks like you have a recently updated Mac OS X with X11 provided by Apple. The X11 display by Apple is to blame -- something like 3 weeks ago it stopped supporting symbol copy-paste in XEmacs as it seems. It does not matter if XEmacs is run locally on the Mac or remotely on a Linux box, with local display on Mac OS.

I can imagine that both Apple and XEmacs maintainers have screwed it up -- if there are any XEmacs maintainers left at all. You could try to install a different X11 for Mac OS, such as http://xquartz.macosforge.org/

Note that on Mac OS, GNU Emacs 22/23 is represented by Aquamacs and Carbon Emacs, which both work somehow.


	Makarius





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