[isabelle-dev] Mac App

[Makarius]

On Mon, 23 Jul 2012, Lawrence Paulson wrote:

> What does Platypus actually give us?

See its website, via the URL from my Admin/MacOS/App1/README: 
http://www.sveinbjorn.org/platypus

   Platypus is a developer tool for the Mac OS X operating system. It can
   be used to create native Mac OS X applications from interpreted scripts
   such as shell scripts or Perl, Ruby and Python programs. This is done by
   wrapping the script in an application bundle along with a native
   executable binary that runs the script.

Some years ago, you had introduced the first Isabelle.app via Platypus 
yourself, which you had still called a "joke" back then.  Over the years, 
I have turned it into what is now part of the official release.

When updating to Platypus 4.7 two days ago, I merely spent 1-2 h to see if 
the situation is basically still the same, i.e. that it is still a 
contemporary way to ship a shell script as MacOS application.  This seems 
to be the case.


> Once we know how the application should be laid out inside, we don't 
> need Platypus any more. The application can be the same every time, just 
> with a fresh copy of Isabelle.

So where are the secret websites explaining this?  As far as I know, Apple 
requires some excutable wrapper for an application.  This is what Platypus 
generates for us, and then hands over to /bin/bash.

Once that Java 7 (or 8) is really there it might be worth trying to skip 
the shell script, and use a Scala entry point like isabelle.Main or 
isabelle.GUI_Setup directly, and add the required things to make it into a 
real Mac application.  For example, this means to stay resident and accept 
documents to be openend while running; in contrast to the crude way to 
start a new instance of the application everytime the users clicks on one 
of its documents.

And again, the question of Proof General / Emacs is related to this.  I 
have handed over its maintenance, but have no plans to destroy it. 
Fundamental changes in the application startup might be in conflict with 
its wiring of Emacs.app.  I am waiting to see with what you as Isabelle 
Proof General maintainers are coming up towards the next release; 
different versions of Emacs.app might behave differently here.


 	Makarius