--- a/.hgignore Fri Jul 03 23:29:03 2009 +0200
+++ b/.hgignore Sat Jul 04 07:58:34 2009 +0200
@@ -17,9 +17,11 @@
^doc-src/.*\.dvi
^doc-src/.*\.idx
^doc-src/.*\.ind
+^doc-src/.*\.lof
^doc-src/.*\.log
^doc-src/.*\.out
^doc-src/.*\.rai
^doc-src/.*\.rao
^doc-src/.*\.toc
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/App1/README Sat Jul 04 07:58:34 2009 +0200
@@ -0,0 +1,9 @@
+Isabelle application bundle for MacOS
+=====================================
+
+Requirements:
+
+* CocoaDialog 2.2.1 http://cocoadialog.sourceforge.net/
+
+* Platypus 4.0 http://www.sveinbjorn.org/platypus
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/App1/mk Sat Jul 04 07:58:34 2009 +0200
@@ -0,0 +1,18 @@
+#!/bin/bash
+#
+# Make Isabelle application bundle
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+
+PLATYPUS_APP="/Applications/Platypus-4.0/Platypus.app"
+COCOADIALOG_APP="/Applications/CocoaDialog.app"
+
+"$PLATYPUS_APP/Contents/Resources/platypus" \
+ -a Isabelle -u Isabelle \
+ -I "de.tum.in.isabelle" \
+ -i "$THIS/../isabelle.icns" \
+ -p /bin/bash \
+ -c "$THIS/script" \
+ -o None \
+ -f "$COCOADIALOG_APP" \
+ "$PWD/Isabelle.app"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/App1/script Sat Jul 04 07:58:34 2009 +0200
@@ -0,0 +1,78 @@
+#!/bin/bash
+#
+# Author: Makarius
+#
+# Isabelle application wrapper
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+THIS_APP="$(cd "$THIS/../.."; pwd)"
+SUPER_APP="$(cd "$THIS/../../.."; pwd)"
+
+
+# sane environment defaults
+cd "$HOME"
+PATH="$PATH:/opt/local/bin"
+
+
+# settings support
+
+function choosefrom ()
+{
+ local RESULT=""
+ local FILE=""
+
+ for FILE in "$@"
+ do
+ [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
+ done
+
+ [ -z "$RESULT" ] && RESULT="$FILE"
+ echo "$RESULT"
+}
+
+
+# Isabelle
+
+ISABELLE_TOOL="$(choosefrom \
+ "$THIS/Isabelle/bin/isabelle" \
+ "$SUPER_APP/Isabelle/bin/isabelle" \
+ "$HOME/bin/isabelle" \
+ isabelle)"
+
+
+# Proof General / Emacs
+
+PROOFGENERAL_EMACS="$(choosefrom \
+ "$THIS/Emacs.app/Contents/MacOS/Emacs" \
+ "$SUPER_APP/Emacs.app/Contents/MacOS/Emacs" \
+ /Applications/Emacs.app/Contents/MacOS/Emacs \
+ "")"
+
+if [ -n "$PROOFGENERAL_EMACS" ]; then
+ EMACS_OPTIONS="-p $PROOFGENERAL_EMACS"
+fi
+
+
+# run interface with error feedback
+
+OUTPUT="/tmp/isabelle$$.out"
+
+( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1
+RC=$?
+
+if [ "$RC" != 0 ]; then
+ echo >> "$OUTPUT"
+ echo "Return code: $RC" >> "$OUTPUT"
+fi
+
+if [ $(stat -f "%z" "$OUTPUT") != 0 ]; then
+ "$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" textbox \
+ --title "Isabelle" \
+ --informative-text "Isabelle output" \
+ --text-from-file "$OUTPUT" \
+ --button1 "OK"
+fi
+
+rm -f "$OUTPUT"
+
+exit "$RC"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/App2/Isabelle.app/Contents/Info.plist Sat Jul 04 07:58:34 2009 +0200
@@ -0,0 +1,46 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
+<plist version="1.0">
+<dict>
+ <key>CFBundleDevelopmentRegion</key>
+ <string>English</string>
+ <key>CFBundleExecutable</key>
+ <string>Isabelle</string>
+ <key>CFBundleGetInfoString</key>
+ <string>Isabelle</string>
+ <key>CFBundleIconFile</key>
+ <string>isabelle.icns</string>
+ <key>CFBundleIdentifier</key>
+ <string>de.tum.in.isabelle</string>
+ <key>CFBundleInfoDictionaryVersion</key>
+ <string>6.0</string>
+ <key>CFBundleName</key>
+ <string>Isabelle</string>
+ <key>CFBundlePackageType</key>
+ <string>APPL</string>
+ <key>CFBundleShortVersionString</key>
+ <string>2009</string>
+ <key>CFBundleSignature</key>
+ <string>????</string>
+ <key>CFBundleVersion</key>
+ <string>2009</string>
+ <key>Java</key>
+ <dict>
+ <key>JVMVersion</key>
+ <string>1.5+</string>
+ <key>VMOptions</key>
+ <string>-Xmx384M</string>
+ <key>ClassPath</key>
+ <string>$JAVAROOT/isabelle-scala.jar</string>
+ <key>MainClass</key>
+ <string>isabelle.GUI_Setup</string>
+ <key>Properties</key>
+ <dict>
+ <key>isabelle.home</key>
+ <string>$APP_PACKAGE/Contents/Resources/Isabelle</string>
+ <key>apple.laf.useScreenMenuBar</key>
+ <string>true</string>
+ </dict>
+ </dict>
+</dict>
+</plist>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/App2/Isabelle.app/Contents/MacOS/Isabelle Sat Jul 04 07:58:34 2009 +0200
@@ -0,0 +1,1 @@
+/System/Library/Frameworks/JavaVM.framework/Resources/MacOS/JavaApplicationStub
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/App2/README Sat Jul 04 07:58:34 2009 +0200
@@ -0,0 +1,7 @@
+Isabelle/JVM application bundle for MacOS
+=========================================
+
+* http://developer.apple.com/documentation/Java/Conceptual/Java14Development/03-JavaDeployment/JavaDeployment.html
+
+* http://developer.apple.com/documentation/Java/Reference/Java_InfoplistRef/Articles/JavaDictionaryInfo.plistKeys.html#//apple_ref/doc/uid/TP40001969
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/App2/mk Sat Jul 04 07:58:34 2009 +0200
@@ -0,0 +1,12 @@
+#!/bin/bash
+#
+# Make Isabelle/JVM application bundle
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+
+APP="$THIS/Isabelle.app"
+
+mkdir -p "$APP/Contents/Resources/Java"
+cp "$THIS/../../../lib/classes/isabelle-scala.jar" "$APP/Contents/Resources/Java"
+cp "$THIS/../isabelle.icns" "$APP/Contents/Resources"
+
--- a/Admin/MacOS/README Fri Jul 03 23:29:03 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-Isabelle application bundle for MacOS
-=====================================
-
-Requirements:
-
-* CocoaDialog 2.2.1 http://cocoadialog.sourceforge.net/
-
-* Platypus 4.0 http://www.sveinbjorn.org/platypus
-
--- a/Admin/MacOS/mk Fri Jul 03 23:29:03 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-#!/bin/bash
-#
-# Make Isabelle application bundle
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-PLATYPUS_APP="/Applications/Platypus-4.0/Platypus.app"
-COCOADIALOG_APP="/Applications/CocoaDialog.app"
-
-"$PLATYPUS_APP/Contents/Resources/platypus" \
- -a Isabelle -u Isabelle \
- -I "de.tum.in.isabelle" \
- -i "$THIS/isabelle.icns" \
- -p /bin/bash \
- -c "$THIS/script" \
- -o None \
- -f "$COCOADIALOG_APP" \
- "$PWD/Isabelle.app"
--- a/Admin/MacOS/script Fri Jul 03 23:29:03 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-#!/bin/bash
-#
-# Author: Makarius
-#
-# Isabelle application wrapper
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-THIS_APP="$(cd "$THIS/../.."; pwd)"
-SUPER_APP="$(cd "$THIS/../../.."; pwd)"
-
-
-# sane environment defaults
-cd "$HOME"
-PATH="$PATH:/opt/local/bin"
-
-
-# settings support
-
-function choosefrom ()
-{
- local RESULT=""
- local FILE=""
-
- for FILE in "$@"
- do
- [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
- done
-
- [ -z "$RESULT" ] && RESULT="$FILE"
- echo "$RESULT"
-}
-
-
-# Isabelle
-
-ISABELLE_TOOL="$(choosefrom \
- "$THIS/Isabelle/bin/isabelle" \
- "$SUPER_APP/Isabelle/bin/isabelle" \
- "$HOME/bin/isabelle" \
- isabelle)"
-
-
-# Proof General / Emacs
-
-PROOFGENERAL_EMACS="$(choosefrom \
- "$THIS/Emacs.app/Contents/MacOS/Emacs" \
- "$SUPER_APP/Emacs.app/Contents/MacOS/Emacs" \
- /Applications/Emacs.app/Contents/MacOS/Emacs \
- "")"
-
-if [ -n "$PROOFGENERAL_EMACS" ]; then
- EMACS_OPTIONS="-p $PROOFGENERAL_EMACS"
-fi
-
-
-# run interface with error feedback
-
-OUTPUT="/tmp/isabelle$$.out"
-
-( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1
-RC=$?
-
-if [ "$RC" != 0 ]; then
- echo >> "$OUTPUT"
- echo "Return code: $RC" >> "$OUTPUT"
-fi
-
-if [ $(stat -f "%z" "$OUTPUT") != 0 ]; then
- "$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" textbox \
- --title "Isabelle" \
- --informative-text "Isabelle output" \
- --text-from-file "$OUTPUT" \
- --button1 "OK"
-fi
-
-rm -f "$OUTPUT"
-
-exit "$RC"
--- a/src/Pure/System/gui_setup.scala Fri Jul 03 23:29:03 2009 +0200
+++ b/src/Pure/System/gui_setup.scala Sat Jul 04 07:58:34 2009 +0200
@@ -43,9 +43,6 @@
}
// values
- if (Platform.is_windows) {
- text.append("Cygwin root: " + Cygwin.config()._1 + "\n")
- }
Platform.defaults match {
case None =>
case Some((name, None)) => text.append("Platform: " + name + "\n")
@@ -53,7 +50,15 @@
text.append("Main platform: " + name1 + "\n")
text.append("Alternative platform: " + name2 + "\n")
}
- text.append("Isabelle home: " + java.lang.System.getProperty("isabelle.home"))
+ if (Platform.is_windows) {
+ text.append("Cygwin root: " + Cygwin.config()._1 + "\n")
+ }
+ try {
+ val isabelle_system = new Isabelle_System
+ text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
+ } catch {
+ case e: RuntimeException => text.append(e.getMessage + "\n")
+ }
// reactions
listenTo(ok)
--- a/src/Pure/System/isabelle_system.scala Fri Jul 03 23:29:03 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala Sat Jul 04 07:58:34 2009 +0200
@@ -80,18 +80,19 @@
val env0 = Map(java.lang.System.getenv.toList: _*)
- val isabelle =
- env0.get("ISABELLE_TOOL") match {
+ val isabelle_home =
+ env0.get("ISABELLE_HOME") match {
case None | Some("") =>
- val isabelle = java.lang.System.getProperty("isabelle.tool")
- if (isabelle == null || isabelle == "") "isabelle"
- else isabelle
- case Some(isabelle) => isabelle
+ val path = java.lang.System.getProperty("isabelle.home")
+ if (path == null || path == "") error("Unknown Isabelle home directory")
+ else path
+ case Some(path) => path
}
val dump = File.createTempFile("isabelle", null)
try {
- val cmdline = shell_prefix ::: List(isabelle, "getenv", "-d", dump.toString)
+ val cmdline = shell_prefix :::
+ List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
val proc = Isabelle_System.raw_execute(env0, true, cmdline: _*)
val (output, rc) = Isabelle_System.process_output(proc)
if (rc != 0) error(output)