[isabelle-dev] Mac App

[Lawrence Paulson]

I forgot that it also generated a binary. If it's just moving a bunch of files into fixed positions, a little script could do that easily.

I'm annoyed because my modifications still do not cause theory files to have an appropriate icon. This used to work.

What would be involved in testing your changesets? Is there some command to generate a Mac application?

Larry

On 25 Jul 2012, at 10:36, Makarius wrote:

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