[isabelle-dev] Mac App

Lawrence Paulson lp15 at cam.ac.uk
Mon Jul 23 18:47:36 CEST 2012


Thanks from all information!

By “today" do you mean literally today, or the 2012 release? I'm puzzled that you have two things released today.

I just made the two small changes mentioned in my e-mail, and they allow drag-and-drop. I don't see document icons working yet, which is puzzling, because they worked with the old application.

I didn't do this with platypus. I just did it. I looked up somewhere how you get icons for documents and how you associate them with applications.

The issue of multiple applications winning is a classic one on any Mac, and users should be able to know how to deal with that.

Larry

On 23 Jul 2012, at 17:41, Makarius wrote:

> 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




More information about the isabelle-dev mailing list