Re: [isabelle] InstallProblem with Proofgeneral



On Mon, 15 Dec 2008, Peter Ulrich wrote:

> 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"

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






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