1 year ago

#366024

test-img

snufkin26

Isabelle/jEdit just starts with ~/Scratch.thy (or does not launch) by clicking .thy file or using open command in MacOS

Recently, I restarted playing with Isabelle/HOL. However, I faced the following problem in MacOS (Monterey): When I click foo.thy file, Isabelle/jEdit launches but ignores foo.thy and starts with ~/Scratch.thy. The same happens when I uses open foo.thy from terminal.

(Also, in MacOS Catalina, Isabelle/jEdit cannot be launched by clicking a file (it tries to launch in the sense that the icon hops in Dock, but after some seconds, it stops), though I cannot re-check it since I've already upgraded MacOS.)

How can I open a theory file by clicking the file?

Some additional information (these are under Monterey):

  1. My Isabelle/jEdit is of Isabelle2021-1 from Isabelle's official site.
  2. I checked Isabelle/jEdit can be launched by clicking Isabelle2021-1.app.
  3. After launching Isabelle/jEdit, I can open files from File > Open... in the Menu bar.
  4. I can open foo.thy directly by /Applications/Isabelle2021-1.app/bin/isabelle jedit foo.thy.
  5. When I launch by clicking a file named Chapter01.thy, then the activity log includes
12:06:08 PM [main] [message] jEdit: starting with command line arguments: -settings=/Users/suzuyu/.isabelle/Isabelle2021-1/jedit -server=Isabelle2021-1 -reuseview -nobackground -nosplash -log=9 /Users/suzuyu/Scratch.thy

so, it seems that the file is already ignored at this stage.

macos

isabelle

0 Answers

Your Answer

Accepted video resources