[isabelle-dev] Mac App
makarius at sketis.net
Wed Jul 25 11:36:59 CEST 2012
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:
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.
More information about the isabelle-dev