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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and