--- a/.hgtags Fri Apr 17 08:35:23 2009 +0200
+++ b/.hgtags Fri Apr 17 08:36:18 2009 +0200
@@ -25,3 +25,4 @@
fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
613c2eb8aef60d016a427011bd8236519b22209a isa2009-test
dda08b76fa999333af77a2afa08aef09cbcd34d2 isa2009-test
+d394a17d4fdb666595c6c3083ce8aee4bba1a1f4 isa2009-test
--- a/Admin/MacOS/README Fri Apr 17 08:35:23 2009 +0200
+++ b/Admin/MacOS/README Fri Apr 17 08:36:18 2009 +0200
@@ -3,15 +3,7 @@
Requirements:
-* CocoaDialog http://cocoadialog.sourceforge.net/
-
-* Platypus http://www.sveinbjorn.org/platypus
-
-* AppHack 1.1 http://www.sveinbjorn.org/apphack
+* CocoaDialog 2.2.1 http://cocoadialog.sourceforge.net/
- Manual setup:
- File type: "Isabelle theory"
- Icon: "theory.icns"
- "Editor"
- Suffixes: "thy"
+* Platypus 4.0 http://www.sveinbjorn.org/platypus
--- a/Admin/MacOS/mk Fri Apr 17 08:35:23 2009 +0200
+++ b/Admin/MacOS/mk Fri Apr 17 08:36:18 2009 +0200
@@ -11,7 +11,6 @@
-a Isabelle -u Isabelle \
-I "de.tum.in.isabelle" \
-i "$THIS/isabelle.icns" \
- -D -X thy \
-p /bin/bash \
-c "$THIS/script" \
-o None \
--- a/src/HOL/Tools/atp_wrapper.ML Fri Apr 17 08:35:23 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Fri Apr 17 08:36:18 2009 +0200
@@ -68,7 +68,7 @@
val fname = File.platform_path probfile
val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy
val cmdline =
- if File.exists cmd then File.shell_path cmd ^ " " ^ args
+ if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
else error ("Bad executable: " ^ Path.implode cmd)
val (proof, rc) = system_out (cmdline ^ " " ^ fname)