[isabelle-dev] Mac App

[Makarius]

On Mon, 23 Jul 2012, Lawrence Paulson wrote:

> Recent Isabelle applications for Mac don't seem to recognise the .thy 
> filename extension, and Mac OS is unwilling to assign them as the 
> default application for theory files. I believe that the fix is as 
> follows:
>
> (1), to use the attached version of Info.plist and
>
> (2), to include the attached icon file (for theory files, which is 
> different from the application icon) in the Resources folder.

This already has a longer history.  Around 2008 I had picked up your 
experimental .app to include it into the official Isabelle distribution, 
in a manner that works for most users.

See Admin/MacOS/App1 in current Isabelle/4ad6182d5bb9.  The README and mk 
define a documented and repeatabke procedure to create Isabelle.app, 
without hand-editing.

Some notes on the history of this:

   (1) http://isabelle.in.tum.de/repos/isabelle/rev/de5b29c25af9 (2008)
     first systematic attempt based on your initial experiments

   (2) http://isabelle.in.tum.de/repos/isabelle/rev/ca28610a0e7e (2008)
     attempt to support .thy file type via AppHack 1.1

   (3) http://isabelle.in.tum.de/repos/isabelle/rev/9343d4b7c5bf (2009)
     give up file type / dropability for now -- does not work reliably

   (4) http://isabelle.in.tum.de/repos/isabelle/rev/6d9c43f51e60 (today)
     updated to Platypus 4.7

   (5) http://isabelle.in.tum.de/repos/isabelle/rev/4ad6182d5bb9 (today)
     try droppable application using Platypus functionality -- in contrast
     to earlier AppHack (cf. 9343d4b7c5bf)

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.)

Current (5) is an experiment to see what it does.  As far as I can tell on 
the spot, it allows to drop .thy files on the application icon, e.g. in 
the finder or dock.

Maybe you find out more, so that we can make some actual progress with 
production quality .app bundling.


(At some later stage one might try to give up Platypus, and make the thing 
a native application based on the JVM app wrapper, in the relative sense 
of "native" for Java on Mac OS -- things are again changing with Java 7.)


 	Makarius