Email Gateway (Aug 18 2022 at 12:46): Email Gateway (Aug 18 2022 at 12:46):From: Peter Ulrich <Peter.Ulrich1975@gmx.de>
Hi,
I have installed xemacs 21.4.21 installed.
I have downloaded and installed the files from the Isabelle website.
When running
/usr/local/Isabelle/bin/Isabelle -p xemacs
xemacs opens together with PG;
when I try to make a step (e.g., next) I get the error:
"Symbol's value as variable is void: proof-toolbar-next"
when trying to enable x-symbol, I get the message:
"Symbol's function definition is void: quail-define-package"
when disabling x-symbol and enabling it again I get:
"Wrong type argument: arrayp, nil"
Email Gateway (Aug 18 2022 at 12:47):From: Makarius <makarius@sketis.net>
This looks like the usual Emacs compatibility problems of Proof General.
Even though XEmacs is still advertized as default for Isabelle2008, GNU
Emacs 22 works usually better.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC