Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2025-RC2 UI possible error

Email Gateway (Feb 14 2025 at 22:13):

From: "John F. Hughes" <jfh@cs.brown.edu>
When on my Mac Mini M1 running Sequoia 15.1.1, double-click on a theory
file via the Finder, Isabelle 2025 opens (and shows Scratch.thy), but it
does not show my theory file.

This is true in 2024 and 2023 as well, and I've always just figured it was
a design choice or something, and lived with it. But since you asked for
feedback, I thought that I might as well mention it. It's certainly
inconsistent with the behaviour of most applications on the Mac, and with
the actual text of the menu (right click on theory file) that says "Open
with..." and let's me select Isabelle2025-RC2.

Sorry to have taken so long to get around to reporting this.

Email Gateway (Feb 15 2025 at 14:38):

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
This is not really a fix (Isabelle does not seems to process 'odoc' Apple events), but I have been using the following script for several years in order to open theory files with Isabelle:

property ISABELLE : "Isabelle2025-RC2"

on open (doc)
do shell script "open -a " & ISABELLE
try
do shell script "/Applications/" & ISABELLE & ".app/bin/isabelle jedit_client " & the quoted form of POSIX path of doc
on error errMsg number errNum
-- If Isabelle is not yet ready, wait 2s
delay 2
try
do shell script "/Applications/" & ISABELLE & ".app/bin/isabelle jedit_client " & the quoted form of POSIX path of doc
on error errMsg number errNum
-- If Isabelle is still not ready, wait 5s again a last time
delay 5
do shell script "/Applications/" & ISABELLE & ".app/bin/isabelle jedit_client " & the quoted form of POSIX path of doc
end try
end try
end open

on run
do shell script "open -a " & ISABELLE
end run

Save this in a file named for instance "IsabelleJEdit2025.applescript", open it in Apple's script editor, adapt the value of the "ISABELLE" property at the beginning of the script to the name of the Isabelle application you want to use, then export it as an application.

The export dialog should look like (it is in French on my computer, but you should select the "Application" format):



You should now be able to open theory files in Isabelle by dropping them on this application.

You can go even further by copying the icon from the Isabelle application into the Contents/Resources folder inside this application bundle, replacing the droplet.icns file with it.
You can find this icon by displaying the contents of the Isabelle application bundle (this is available in the contextual menu when you right-click or control-click on the application in the Finder), then looking for isabelle.icns in Contents/Resources.

If you associate .thy files to this application, you will be able to open theory files in Isabelle just by double-clicking on them in the Finder.

You have to build this application yourself on your computer because the security restrictions on the execution of applications make it very difficult to distribute this kind of code in a ready to run form.

You can also build several applications, with different values of the ISABELLE property, that open theory files in different versions of Isabelle.

In the same vein, if you are using Linux, you can create an Isabelle.desktop file with the following contents:

[Desktop Entry]
Version=1.0
Name=Isabelle
GenericName=Proof assistant
Exec=/usr/local/Isabelle2025/bin/isabelle jedit %F
StartupNotify=true
Terminal=false
Icon=/usr/local/Isabelle2025/lib/icons/isabelle.xpm
Type=Application
Categories=Proof;Development;Science;Math
MimeType=text/text;

adjusting for the location of your installation of Isabelle in the Exec and Icon entries.

Regards,

Frédéric

Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire Méthodes Formelles (LMF)
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 75 31 78 32‬

Le 14 févr. 2025 à 23:13, John F. Hughes <jfh@cs.brown.edu> a écrit :

When on my Mac Mini M1 running Sequoia 15.1.1, double-click on a theory file via the Finder, Isabelle 2025 opens (and shows Scratch.thy), but it does not show my theory file.

This is true in 2024 and 2023 as well, and I've always just figured it was a design choice or something, and lived with it. But since you asked for feedback, I thought that I might as well mention it. It's certainly inconsistent with the behaviour of most applications on the Mac, and with the actual text of the menu (right click on theory file) that says "Open with..." and let's me select Isabelle2025-RC2.

Sorry to have taken so long to get around to reporting this.

Capture d’écran 2025-02-15 à 14.54.01.png

Email Gateway (Feb 15 2025 at 14:45):

From: "John F. Hughes" <jfh@cs.brown.edu>
Thank you! This kind of scripting is new to me. (I knew it had to be
available, but never really looked into it.) Thanks for saving me a bunch
of work.

--John

On Sat, Feb 15, 2025 at 9:30 AM Frédéric Boulanger <
frederic.boulanger@centralesupelec.fr> wrote:

This is not really a fix (Isabelle does not seems to process 'odoc' Apple
events), but I have been using the following script for several years in
order to open theory files with Isabelle:

property ISABELLE : "Isabelle2025-RC2"

on open (doc)

do shell script "open -a " & ISABELLE

try

do shell script "/Applications/" & ISABELLE & ".app/bin/isabelle
jedit_client " & the quoted form of POSIX path of doc

on error errMsg number errNum

-- If Isabelle is not yet ready, wait 2s

delay 2

try

do shell script "/Applications/" & ISABELLE & ".app/bin/isabelle
jedit_client " & the quoted form of POSIX path of doc

on error errMsg number errNum

-- If Isabelle is still not ready, wait 5s again a last time

delay 5

do shell script "/Applications/" & ISABELLE & ".app/bin/isabelle
jedit_client " & the quoted form of POSIX path of doc

end try

end try

end open

on run

do shell script "open -a " & ISABELLE

end run

Save this in a file named for instance "IsabelleJEdit2025.applescript",
open it in Apple's script editor, adapt the value of the "ISABELLE"
property at the beginning of the script to the name of the Isabelle
application you want to use, then export it as an application.

The export dialog should look like (it is in French on my computer, but
you should select the "Application" format):

[image: Capture d’écran 2025-02-15 à 14.54.01.png]

You should now be able to open theory files in Isabelle by dropping them
on this application.

You can go even further by copying the icon from the Isabelle application
into the Contents/Resources folder inside this application bundle,
replacing the droplet.icns file with it.
You can find this icon by displaying the contents of the Isabelle
application bundle (this is available in the contextual menu when you
right-click or control-click on the application in the Finder), then
looking for isabelle.icns in Contents/Resources.

If you associate .thy files to this application, you will be able to open
theory files in Isabelle just by double-clicking on them in the Finder.

You have to build this application yourself on your computer because the
security restrictions on the execution of applications make it very
difficult to distribute this kind of code in a ready to run form.

You can also build several applications, with different values of the
ISABELLE property, that open theory files in different versions of Isabelle.

In the same vein, if you are using Linux, you can create an
Isabelle.desktop file with the following contents:

---

[Desktop Entry]
Version=1.0
Name=Isabelle
GenericName=Proof assistant
Exec=/usr/local/Isabelle2025/bin/isabelle jedit %F
StartupNotify=true
Terminal=false
Icon=/usr/local/Isabelle2025/lib/icons/isabelle.xpm
Type=Application
Categories=Proof;Development;Science;Math
MimeType=text/text;

---

adjusting for the location of your installation of Isabelle in the Exec
and Icon entries.

Regards,

Frédéric

Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire Méthodes
Formelles (LMF)
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond
Castaing, 91190 Gif-sur-Yvette
+33 [0]1 75 31 78 32‬

Le 14 févr. 2025 à 23:13, John F. Hughes <jfh@cs.brown.edu> a écrit :

When on my Mac Mini M1 running Sequoia 15.1.1, double-click on a theory
file via the Finder, Isabelle 2025 opens (and shows Scratch.thy), but it
does not show my theory file.

This is true in 2024 and 2023 as well, and I've always just figured it was
a design choice or something, and lived with it. But since you asked for
feedback, I thought that I might as well mention it. It's certainly
inconsistent with the behaviour of most applications on the Mac, and with
the actual text of the menu (right click on theory file) that says "Open
with..." and let's me select Isabelle2025-RC2.

Sorry to have taken so long to get around to reporting this.

Capture d’écran 2025-02-15 à 14.54.01.png

Last updated: Mar 09 2025 at 12:28 UTC