merged
authorhaftmann
Sat, 04 Jul 2009 07:58:34 +0200
changeset 31939 e1ac7ab73bb1
parent 31928 2d8e50886558 (diff)
parent 31938 f193d95b4632 (current diff)
child 31940 5fe21cac6bf7
merged
src/HOL/Nominal/nominal.ML
--- 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)