Re: [isabelle] isatool wanted by proofgeneral?
Just to be sure, I have commented out the load-file line from my .emacs
file, and when I run isabelle emacs there is no change in behavior, as
indeed some examination of the scripts would indicate there shouldn't be.
On both machines I was installing a totally fresh copy of
Isabelle-2009-1. There is no other isabelle anywhere on either of these
machines. On one of them there never has been any other copy of Isabelle.
I've done a bit of further investigation and found that all of the code
referring to isatool is located in
ProofGeneral/isar/interface-setup.el. However, as cursory inspection
seemed to indicate that this file was the same as the one bundled in
the mac distribution, with which I have no problem. Therefore, I assume
my problem involves something more.
I have included below the *Messages* log from starting up isabelle emacs
on a totally generic linux box, in case it might be of assistance to
anyone who might be able to help me.
-l /usr/local/Isabelle2009-1/etc/isar-keywords.el -l
For information about the GNU Project and its goals, type C-h C-p.
File not found and directory write-protected
Loading isar (source)...
Loading proof-splash (source)...done
Loading isar (source)...done
Loading proof-script (source)...
Loading proof-menu (source)...done
Loading proof-script (source)...done
Loading proof-toolbar (source)...done
File mode specification error: (void-variable image-load-path)
On Sun, 17 Jan 2010, Elsa L Gunter wrote:
I have added the (load-file "<proofgeneral_home>/generic/proof-site.el")
line to my .emacs file. When I go to start up Isabelle by
"Please give the full path to `isatool' (RET if you don't have it): <cwd>"
When using the regular "isabelle emacs" wrapper, their is no need to load
proof-site.el manually, and doing so might cause the problem (there might
be other reasons).
This archive was generated by a fusion of
Pipermail (Mailman edition) and