# HG changeset patch # User haftmann # Date 1246687114 -7200 # Node ID e1ac7ab73bb154cf80b264a9877978ee0b9bf27f # Parent 2d8e508865589eb045233864c580b2ac1b911d27# Parent f193d95b4632789ac853247ec92c826f6a362767 merged diff -r f193d95b4632 -r e1ac7ab73bb1 .hgignore --- 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 + diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/App1/README --- /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 + diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/App1/mk --- /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" diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/App1/script --- /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" diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/App2/Isabelle.app/Contents/Info.plist --- /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 @@ + + + + + CFBundleDevelopmentRegion + English + CFBundleExecutable + Isabelle + CFBundleGetInfoString + Isabelle + CFBundleIconFile + isabelle.icns + CFBundleIdentifier + de.tum.in.isabelle + CFBundleInfoDictionaryVersion + 6.0 + CFBundleName + Isabelle + CFBundlePackageType + APPL + CFBundleShortVersionString + 2009 + CFBundleSignature + ???? + CFBundleVersion + 2009 + Java + + JVMVersion + 1.5+ + VMOptions + -Xmx384M + ClassPath + $JAVAROOT/isabelle-scala.jar + MainClass + isabelle.GUI_Setup + Properties + + isabelle.home + $APP_PACKAGE/Contents/Resources/Isabelle + apple.laf.useScreenMenuBar + true + + + + diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/App2/Isabelle.app/Contents/MacOS/Isabelle --- /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 diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/App2/README --- /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 + diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/App2/mk --- /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" + diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/README --- 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 - diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/mk --- 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" diff -r f193d95b4632 -r e1ac7ab73bb1 Admin/MacOS/script --- 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" diff -r f193d95b4632 -r e1ac7ab73bb1 src/Pure/System/gui_setup.scala --- 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) diff -r f193d95b4632 -r e1ac7ab73bb1 src/Pure/System/isabelle_system.scala --- 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)