Email Gateway (Aug 18 2022 at 13:46): Email Gateway (Aug 18 2022 at 13:46):From: John Matthews <matthews@galois.com>
I need to use Isabelle2008 for a particular project. I'd prefer to use
xemacs, assuming it was still supported for this version of Isabelle.
Which versions of xemacs and ProofGeneral work best on Isabelle2008?
Thanks,
-john
Email Gateway (Aug 18 2022 at 13:46):From: Makarius <makarius@sketis.net>
It only depends on the version of Proof General you are using. You can
use the same one for Isabelle2008 and Isabelle2009, which is still 3.7.1
as offered on the Isabelle2009 download site. Thus the explanations on
http://isabelle.in.tum.de/installation.html also apply, as far as Emacs is
concerned.
XEmacs is a dying platform, but some versions on some platforms still
happen to work with PG 3.7.1. E.g. XEmacs 21.4.20 or similar, but only on
Linux. There are many problems on Mac OS and Cygwin.
GNU Emacs 22 usually works best.
Makarius
Email Gateway (Aug 18 2022 at 13:47):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 13:48):From: John Matthews <matthews@galois.com>
Thanks for the 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/
I just tried this but no luck, copy/paste still doesn't work correctly.
Note that on Mac OS, GNU Emacs 22/23 is represented by Aquamacs and
Carbon Emacs, which both work somehow.
I tried these versions out, but the xsymbol keyboard shortcuts I'm
used to don't work there, at least with Isabelle2008.
It was still worth a try...
-john
Email Gateway (Aug 18 2022 at 13:48):From: Gerwin Klein <gerwin.klein@nicta.com.au>
John Matthews wrote:
Same problem here, very annoying. I tried going back to the previous xemacs
version in macports, but that didn't help either (haven't tried the
combination yet, though).
You canre-bind keys to x-symbol-copy-region-encoded and x-symbol-yank-decoded,
but I haven't found an equivalent for cut (kill in xemacs speak, I guess) and
it wasn't painful enough yet to write one.
(global-set-key [(meta c)] 'x-symbol-copy-region-encoded)
(global-set-key [(meta v)] 'x-symbol-yank-decoded)
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 13:48):From: John Matthews <matthews@galois.com>
Yep, this works on my system too. Thanks Gerwin...
-john
Email Gateway (Aug 18 2022 at 13:48):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, I didn't know these exist.
On Aquamacs: copy/paste works fine here, but is screwed up by PG: once
PG is loaded, you can no longer cut/paste reliably between the editor
and the outside world :-(
Tobias
Last updated: May 03 2024 at 12:27 UTC