[isabelle-dev] Mac App
makarius at sketis.net
Mon Jul 23 20:36:16 CEST 2012
On Mon, 23 Jul 2012, Lawrence Paulson wrote:
> By “today" do you mean literally today, or the 2012 release? I'm puzzled
> that you have two things released today.
I have merely pushed two changesets:
>> (4) http://isabelle.in.tum.de/repos/isabelle/rev/6d9c43f51e60 (today)
>> (5) http://isabelle.in.tum.de/repos/isabelle/rev/4ad6182d5bb9 (today)
For extra convenience I have added the full URL and some hint about the
dates. The full information is already given by the changeset ids
(abbreviated SHA1 keys), so with the Mercurial front-end of your choice
you can retrieve all these details, and more.
The above merely gives you the updated Admin/MacOS/App1/README and mk
script to repeat the process yourself.
> I just made the two small changes mentioned in my e-mail, and they allow
> drag-and-drop. I don't see document icons working yet, which is
> puzzling, because they worked with the old application.
Here are your edits after according to diff -w:
> <string>Isabelle theory.icns</string>
> <string>Isabelle theory</string>
> I didn't do this with platypus. I just did it.
The Info.plist edited here was generated by Platypus 4.0. The main thing
is the executable application wrapper of Platypus, and the plist needs to
correspond to that. After updating to Platypus 4.7 I've got a different
Info.plist, which was not very surprising.
Editing generated files only works one-shot, not for long-term
> I looked up somewhere how you get icons for documents and how you
> associate them with applications.
Do you have some concrete links with explanations how this works?
> The issue of multiple applications winning is a classic one on any Mac,
> and users should be able to know how to deal with that.
Our situation is not quite classic:
>> The problems leading to (3) were manyfold: unclarity which Isabelle
>> application "wins" when many of them are on the system (which happens
>> routinely); unclarity what happens due to nested applications (Platypus
>> wrapper, Emacs or Java Runtime etc.)
Where "nested" means that the shell script invokes another application,
which was some Emacs.app in 2009 when I disabled the attempt with the
document--application connection at that time, see again
Isabelle/9343d4b7c5bf with the Mercurial changeset browser of your choice.
BTW, since you are now one of the Proof General maintainers, you may have
to understand its integration with Isabelle.app, and potentially find ways
to avoid some of its oddities caused by Isabelle.app invoking Emacs.app
via a shell script.
For Isabelle/jEdit there might be ways in the future to avoid all that,
running more directly some .jar application. But that reform is not
More information about the isabelle-dev