From: Perry Wagle <wagle@mac.com>
Isabelle 2011 for MacOSX comes with its own version of Emacs.app for proof general.
This means that its distinct from the Emacs.app I have already installed even though the two are identical. What's the thinking? Can I combine Isabelle 2011's version with my already installed version using some sort of "emacsclient -c" interface so that I have only one instance of the app running?
-- Perry
From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Perry,
Yes. From the command line, you can specify the -p option to point to any emacs client. For example,
/Applications/Isabelle2011.app/Isabelle/bin/isabelle emacs -p /Applications/Isabelle2009-2.app/Contents/Resources/Emacs.app/Contents/MacOS/Emacs
(all on one line) will launch Isabelle2011 with the Emacs from Isabelle2009-2, assuming the applications are installed at the same places as on my Mac (they should be by default).
Regards,
Jasmin
From: Makarius <makarius@sketis.net>
On Tue, 22 Feb 2011, Perry Wagle wrote:
Isabelle 2011 for MacOSX comes with its own version of Emacs.app for
proof general.This means that its distinct from the Emacs.app I have already installed
even though the two are identical. What's the thinking?
The general idea is to sacrifice some disk space to approximate a fully
integrated application that runs out of the box as far as possible.
Unfortunately there are occasional conflicts with how Mac OS X thinks
about this. For example, after running Isabelle.app it is hard to start an
independent copy of the Emacs.app that happens to be used here.
Can I combine Isabelle 2011's version with my already installed version
using some sort of "emacsclient -c" interface so that I have only one
instance of the app running?
The main plumbing is done in Isabelle2011.app/Contents/Resources/script
which can in principle be customized by ambitious users, but there are
many well-known problems awaiting.
In particular, the version of Emacs and Proof General need to fit together
-- before each official Isabelle release 1-2 weeks are set aside for a
desparate search of a combination that works most of the time.
Using actual "emacsclient" is even more tricky, but not impossible.
Ultimately you need to ensure that the careful environment setup of
Isabelle2011.app/Contents/Resources/script and the general Isabelle
environment is somehow observed by the already running Emacs process.
This might require some Emacs lisp for Proof General initialization.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC