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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
