[isabelle-dev] Mac App

Makarius 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:

>       <key>CFBundleDocumentTypes</key>
>       <array>
>               <dict>
>                       <key>CFBundleTypeExtensions</key>
>                       <array>
>                               <string>thy</string>
>                       </array>
>                       <key>CFBundleTypeIconFile</key>
>                       <string>Isabelle theory.icns</string>
>                       <key>CFBundleTypeName</key>
>                       <string>Isabelle theory</string>
>                       <key>CFBundleTypeRole</key>
>                       <string>Editor</string>
>               </dict>
>       </array>

> 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 mailing list