eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
authorwenzelm
Wed Dec 05 19:42:40 2018 +0100 (19 months ago)
changeset 694017a1b7b737c02
parent 69400 c19b7b565998
child 69402 61f4c406d727
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
more robust components and classpath via Other_Isabelle;
updated macos_app to include full dmg template;
misc tuning and clarification;
Admin/MacOS/Info.plist
Admin/MacOS/Info.plist-part1
Admin/MacOS/Info.plist-part2
Admin/MacOS/README
Admin/MacOS/Resources/en.lproj/Localizable.strings
Admin/MacOS/Resources/isabelle.icns
Admin/MacOS/Resources/theory.icns
Admin/MacOS/dmg/DS_Store
Admin/MacOS/dmg/background.png
Admin/components/bundled-macos
Admin/components/components.sha1
Admin/lib/Tools/makedist_bundle
src/Pure/Admin/build_release.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/isabelle_devel.scala
src/Pure/Admin/other_isabelle.scala
src/Pure/Admin/remote_dmg.scala
src/Pure/System/components.scala
src/Pure/System/isabelle_tool.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/MacOS/Info.plist	Wed Dec 05 19:42:40 2018 +0100
     1.3 @@ -0,0 +1,69 @@
     1.4 +<?xml version="1.0" ?>
     1.5 +<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
     1.6 +<plist version="1.0">
     1.7 +<dict>
     1.8 +<key>CFBundleDevelopmentRegion</key>
     1.9 +<string>English</string>
    1.10 +<key>CFBundleExecutable</key>
    1.11 +<string>JavaAppLauncher</string>
    1.12 +<key>CFBundleIconFile</key>
    1.13 +<string>isabelle.icns</string>
    1.14 +<key>CFBundleIdentifier</key>
    1.15 +<string>de.tum.in.isabelle.{ISABELLE_NAME}</string>
    1.16 +<key>CFBundleDisplayName</key>
    1.17 +<string>{ISABELLE_NAME}</string>
    1.18 +<key>CFBundleInfoDictionaryVersion</key>
    1.19 +<string>6.0</string>
    1.20 +<key>CFBundleName</key>
    1.21 +<string>{ISABELLE_NAME}</string>
    1.22 +<key>CFBundlePackageType</key>
    1.23 +<string>APPL</string>
    1.24 +<key>CFBundleShortVersionString</key>
    1.25 +<string>1.0</string>
    1.26 +<key>CFBundleSignature</key>
    1.27 +<string>????</string>
    1.28 +<key>CFBundleVersion</key>
    1.29 +<string>1</string>
    1.30 +<key>NSHumanReadableCopyright</key>
    1.31 +<string></string>
    1.32 +<key>LSMinimumSystemVersion</key>
    1.33 +<string>10.7</string>
    1.34 +<key>LSApplicationCategoryType</key>
    1.35 +<string>public.app-category.developer-tools</string>
    1.36 +<key>NSHighResolutionCapable</key>
    1.37 +<string>true</string>
    1.38 +<key>NSSupportsAutomaticGraphicsSwitching</key>
    1.39 +<string>true</string>
    1.40 +<key>JVMRuntime</key>
    1.41 +<string>bundled.jdk</string>
    1.42 +<key>JVMMainClassName</key>
    1.43 +<string>isabelle.Main</string>
    1.44 +<key>CFBundleDocumentTypes</key>
    1.45 +<array>
    1.46 +<dict>
    1.47 +<key>CFBundleTypeExtensions</key>
    1.48 +<array>
    1.49 +<string>thy</string>
    1.50 +</array>
    1.51 +<key>CFBundleTypeIconFile</key>
    1.52 +<string>theory.icns</string>
    1.53 +<key>CFBundleTypeName</key>
    1.54 +<string>Isabelle theory file</string>
    1.55 +<key>CFBundleTypeRole</key>
    1.56 +<string>Editor</string>
    1.57 +<key>LSTypeIsPackage</key>
    1.58 +<false/>
    1.59 +</dict>
    1.60 +</array>
    1.61 +<key>JVMOptions</key>
    1.62 +<array>
    1.63 +{JAVA_OPTIONS}
    1.64 +<string>-Dapple.awt.application.name={ISABELLE_NAME}</string>
    1.65 +<string>-Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
    1.66 +<string>-Disabelle.app=true</string>
    1.67 +</array>
    1.68 +<key>JVMArguments</key>
    1.69 +<array>
    1.70 +</array>
    1.71 +</dict>
    1.72 +</plist>
     2.1 --- a/Admin/MacOS/Info.plist-part1	Tue Dec 04 16:11:52 2018 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,59 +0,0 @@
     2.4 -<?xml version="1.0" ?>
     2.5 -<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
     2.6 -<plist version="1.0">
     2.7 -<dict>
     2.8 -<key>CFBundleDevelopmentRegion</key>
     2.9 -<string>English</string>
    2.10 -<key>CFBundleExecutable</key>
    2.11 -<string>JavaAppLauncher</string>
    2.12 -<key>CFBundleIconFile</key>
    2.13 -<string>isabelle.icns</string>
    2.14 -<key>CFBundleIdentifier</key>
    2.15 -<string>de.tum.in.isabelle.{ISABELLE_NAME}</string>
    2.16 -<key>CFBundleDisplayName</key>
    2.17 -<string>{ISABELLE_NAME}</string>
    2.18 -<key>CFBundleInfoDictionaryVersion</key>
    2.19 -<string>6.0</string>
    2.20 -<key>CFBundleName</key>
    2.21 -<string>{ISABELLE_NAME}</string>
    2.22 -<key>CFBundlePackageType</key>
    2.23 -<string>APPL</string>
    2.24 -<key>CFBundleShortVersionString</key>
    2.25 -<string>1.0</string>
    2.26 -<key>CFBundleSignature</key>
    2.27 -<string>????</string>
    2.28 -<key>CFBundleVersion</key>
    2.29 -<string>1</string>
    2.30 -<key>NSHumanReadableCopyright</key>
    2.31 -<string></string>
    2.32 -<key>LSMinimumSystemVersion</key>
    2.33 -<string>10.7</string>
    2.34 -<key>LSApplicationCategoryType</key>
    2.35 -<string>public.app-category.developer-tools</string>
    2.36 -<key>NSHighResolutionCapable</key>
    2.37 -<string>true</string>
    2.38 -<key>NSSupportsAutomaticGraphicsSwitching</key>
    2.39 -<string>true</string>
    2.40 -<key>JVMRuntime</key>
    2.41 -<string>bundled.jdk</string>
    2.42 -<key>JVMMainClassName</key>
    2.43 -<string>isabelle.Main</string>
    2.44 -<key>CFBundleDocumentTypes</key>
    2.45 -<array>
    2.46 -<dict>
    2.47 -<key>CFBundleTypeExtensions</key>
    2.48 -<array>
    2.49 -<string>thy</string>
    2.50 -</array>
    2.51 -<key>CFBundleTypeIconFile</key>
    2.52 -<string>theory.icns</string>
    2.53 -<key>CFBundleTypeName</key>
    2.54 -<string>Isabelle theory file</string>
    2.55 -<key>CFBundleTypeRole</key>
    2.56 -<string>Editor</string>
    2.57 -<key>LSTypeIsPackage</key>
    2.58 -<false/>
    2.59 -</dict>
    2.60 -</array>
    2.61 -<key>JVMOptions</key>
    2.62 -<array>
     3.1 --- a/Admin/MacOS/Info.plist-part2	Tue Dec 04 16:11:52 2018 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,8 +0,0 @@
     3.4 -<string>-Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
     3.5 -<string>-Disabelle.app=true</string>
     3.6 -</array>
     3.7 -<key>JVMArguments</key>
     3.8 -<array>
     3.9 -</array>
    3.10 -</dict>
    3.11 -</plist>
     4.1 --- a/Admin/MacOS/README	Tue Dec 04 16:11:52 2018 +0100
     4.2 +++ b/Admin/MacOS/README	Wed Dec 05 19:42:40 2018 +0100
     4.3 @@ -5,4 +5,3 @@
     4.4  
     4.5    see appbundler-1.0.jar
     4.6    see com/oracle/appbundler/JavaAppLauncher
     4.7 -
     5.1 --- a/Admin/MacOS/Resources/en.lproj/Localizable.strings	Tue Dec 04 16:11:52 2018 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,3 +0,0 @@
     5.4 -"JRELoadError" = "Unable to load Java Runtime Environment.";
     5.5 -"MainClassNameRequired" = "Main class name is required.";
     5.6 -"JavaDirectoryNotFound" = "Unable to enumerate Java directory contents.";
     6.1 Binary file Admin/MacOS/Resources/isabelle.icns has changed
     7.1 Binary file Admin/MacOS/Resources/theory.icns has changed
     8.1 Binary file Admin/MacOS/dmg/DS_Store has changed
     9.1 Binary file Admin/MacOS/dmg/background.png has changed
    10.1 --- a/Admin/components/bundled-macos	Tue Dec 04 16:11:52 2018 +0100
    10.2 +++ b/Admin/components/bundled-macos	Wed Dec 05 19:42:40 2018 +0100
    10.3 @@ -1,2 +1,2 @@
    10.4  #additional components to be bundled for release
    10.5 -macos_app-20130716
    10.6 +macos_app-20181205
    11.1 --- a/Admin/components/components.sha1	Tue Dec 04 16:11:52 2018 +0100
    11.2 +++ b/Admin/components/components.sha1	Wed Dec 05 19:42:40 2018 +0100
    11.3 @@ -151,6 +151,7 @@
    11.4  377e36efb8608e6c828c7718d890e97fde2006a4  linux_app-20131007.tar.gz
    11.5  0aab4f73ff7f5e36f33276547e10897e1e56fb1d  macos_app-20130716.tar.gz
    11.6  ad5d0e640ce3609a885cecab645389a2204e03bb  macos_app-20150916.tar.gz
    11.7 +400af57ec5cd51f96928d9de00d077524a6fe316  macos_app-20181205.tar.gz
    11.8  26df569cee9c2fd91b9ac06714afd43f3b37a1dd  nunchaku-0.3.tar.gz
    11.9  e573f2cbb57eb7b813ed5908753cfe2cb41033ca  nunchaku-0.5.tar.gz
   11.10  fe57793aca175336deea4f5e9c0d949a197850ac  opam-1.2.2.tar.gz
    12.1 --- a/Admin/lib/Tools/makedist_bundle	Tue Dec 04 16:11:52 2018 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,394 +0,0 @@
    12.4 -#!/usr/bin/env bash
    12.5 -#
    12.6 -# DESCRIPTION: re-package Isabelle distribution with add-on components
    12.7 -
    12.8 -## diagnostics
    12.9 -
   12.10 -PRG=$(basename "$0")
   12.11 -
   12.12 -function usage()
   12.13 -{
   12.14 -  echo
   12.15 -  echo "Usage: isabelle $PRG ARCHIVE PLATFORM_FAMILY [REMOTE_MAC]"
   12.16 -  echo
   12.17 -  echo "  Re-package Isabelle source distribution with add-on components and"
   12.18 -  echo "  post-hoc patches for platform family linux, windows, macos."
   12.19 -  echo
   12.20 -  echo "  The optional remote Mac OS X system is used for dmg build."
   12.21 -  echo
   12.22 -  echo "  Add-on components are that of the running Isabelle version!"
   12.23 -  echo
   12.24 -  exit 1
   12.25 -}
   12.26 -
   12.27 -function fail()
   12.28 -{
   12.29 -  echo "$1" >&2
   12.30 -  exit 2
   12.31 -}
   12.32 -
   12.33 -
   12.34 -## arguments
   12.35 -
   12.36 -[ "$#" -ne 2 -a "$#" -ne 3 ] && usage
   12.37 -
   12.38 -ARCHIVE="$1"; shift
   12.39 -PLATFORM_FAMILY="$1"; shift
   12.40 -REMOTE_MAC="$1"; shift
   12.41 -
   12.42 -[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
   12.43 -
   12.44 -ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
   12.45 -ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
   12.46 -
   12.47 -
   12.48 -## main
   12.49 -
   12.50 -#GNU tar (notably on Mac OS X)
   12.51 -type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
   12.52 -
   12.53 -TMP="/var/tmp/isabelle-makedist$$"
   12.54 -mkdir "$TMP" || fail "Cannot create directory $TMP"
   12.55 -
   12.56 -ISABELLE_TARGET="$TMP/$ISABELLE_NAME"
   12.57 -
   12.58 -tar -C "$TMP" -x -z -f "$ARCHIVE" || exit 2
   12.59 -
   12.60 -
   12.61 -# distribution classpath (based on educated guesses)
   12.62 -
   12.63 -splitarray ":" "$ISABELLE_CLASSPATH"; CLASSPATH_ENTRIES=("${SPLITARRAY[@]}")
   12.64 -declare -a DISTRIBUTION_CLASSPATH=()
   12.65 -
   12.66 -for ENTRY in "${CLASSPATH_ENTRIES[@]}"
   12.67 -do
   12.68 -  ENTRY=$(echo "$ENTRY" | perl -n -e "
   12.69 -    if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; }
   12.70 -    elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; }
   12.71 -    elsif (m,/home/isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; }
   12.72 -    else { print; };
   12.73 -    print qq{\n};")
   12.74 -  DISTRIBUTION_CLASSPATH["${#DISTRIBUTION_CLASSPATH[@]}"]="$ENTRY"
   12.75 -done
   12.76 -
   12.77 -DISTRIBUTION_CLASSPATH["${#DISTRIBUTION_CLASSPATH[@]}"]="src/Tools/jEdit/dist/jedit.jar"
   12.78 -
   12.79 -echo "classpath"
   12.80 -for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
   12.81 -do
   12.82 -  echo "  $ENTRY"
   12.83 -done
   12.84 -
   12.85 -
   12.86 -# bundled components
   12.87 -
   12.88 -if [ ! -e "$ARCHIVE_DIR/contrib" ]; then
   12.89 -  if [ ! -e "$ARCHIVE_DIR/../contrib" ]; then
   12.90 -    mkdir -p "$ARCHIVE_DIR/contrib"
   12.91 -  else
   12.92 -    ln -s "../contrib" "$ARCHIVE_DIR/contrib"
   12.93 -  fi
   12.94 -fi
   12.95 -
   12.96 -echo "#bundled components" >> "$ISABELLE_TARGET/etc/components"
   12.97 -
   12.98 -for CATALOG in main "$PLATFORM_FAMILY" bundled "bundled-$PLATFORM_FAMILY"
   12.99 -do
  12.100 -  CATALOG_FILE="$ISABELLE_HOME/Admin/components/$CATALOG"
  12.101 -  if [ -f "$CATALOG_FILE" ]
  12.102 -  then
  12.103 -    echo "catalog ${CATALOG}"
  12.104 -    {
  12.105 -      while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
  12.106 -      do
  12.107 -        case "$REPLY" in
  12.108 -          \#* | "") ;;
  12.109 -          *)
  12.110 -            COMPONENT="$REPLY"
  12.111 -            COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
  12.112 -            case "$COMPONENT" in
  12.113 -              jedit_build*) ;;
  12.114 -              *)
  12.115 -                echo "  component $COMPONENT"
  12.116 -                CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"
  12.117 -                if [ ! -f "$CONTRIB" ]; then
  12.118 -                  type -p curl  > /dev/null || fail "Cannot download files: missing curl"
  12.119 -                  REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz"
  12.120 -                  echo "  downloading $REMOTE"
  12.121 -                  curl --fail --silent "$REMOTE" > "$CONTRIB" || \
  12.122 -                    fail "Failed to download \"$REMOTE\""
  12.123 -                  perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2
  12.124 -                fi
  12.125 -
  12.126 -                tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB" || exit 2
  12.127 -                if [ -f "$COMPONENT_DIR/etc/settings" -o -f "$COMPONENT_DIR/etc/components" ]
  12.128 -                then
  12.129 -                  case "$COMPONENT" in
  12.130 -                    jdk-*)
  12.131 -                      mv "$ISABELLE_TARGET/contrib/$COMPONENT" "$ISABELLE_TARGET/contrib/jdk"
  12.132 -                      echo "contrib/jdk" >> "$ISABELLE_TARGET/etc/components"
  12.133 -                      ;;
  12.134 -                    *)
  12.135 -                      echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
  12.136 -                      ;;
  12.137 -                  esac
  12.138 -                fi
  12.139 -                ;;
  12.140 -            esac
  12.141 -            ;;
  12.142 -        esac
  12.143 -      done
  12.144 -    } < "$CATALOG_FILE"
  12.145 -  fi
  12.146 -done
  12.147 -
  12.148 -
  12.149 -# purge other platforms
  12.150 -
  12.151 -function purge_target
  12.152 -{
  12.153 -  (
  12.154 -    cd "$ISABELLE_TARGET"
  12.155 -    for DIR in $(eval find "$@" | sort)
  12.156 -    do
  12.157 -      echo "removing $DIR"
  12.158 -      rm -rf "$DIR"
  12.159 -    done
  12.160 -  )
  12.161 -}
  12.162 -
  12.163 -
  12.164 -# platform-specific setup (inside archive)
  12.165 -
  12.166 -case "$PLATFORM_FAMILY" in
  12.167 -  linux)
  12.168 -    purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
  12.169 -
  12.170 -    (
  12.171 -      init_component "$JEDIT_HOME"
  12.172 -
  12.173 -      echo "# Java runtime options"
  12.174 -      eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
  12.175 -      for ARG in "${JAVA_ARGS[@]}"
  12.176 -      do
  12.177 -        echo "$ARG"
  12.178 -      done
  12.179 -      echo "-Disabelle.jedit_server=${ISABELLE_NAME}"
  12.180 -    ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.options"
  12.181 -
  12.182 -    LINUX_CLASSPATH=""
  12.183 -    for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
  12.184 -    do
  12.185 -      if [ -z "$LINUX_CLASSPATH" ]; then
  12.186 -        LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY"
  12.187 -      else
  12.188 -        LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY"
  12.189 -      fi
  12.190 -    done
  12.191 -
  12.192 -    cat "$ISABELLE_HOME/Admin/Linux/Isabelle.run" | \
  12.193 -      perl -p > "$ISABELLE_TARGET/${ISABELLE_NAME}.run" -e "s,{CLASSPATH},$LINUX_CLASSPATH,;"
  12.194 -    chmod +x "$ISABELLE_TARGET/${ISABELLE_NAME}.run"
  12.195 -
  12.196 -    mv "$ISABELLE_TARGET/contrib/linux_app" "$TMP/."
  12.197 -    cp "$TMP/linux_app/Isabelle" "$ISABELLE_TARGET/$ISABELLE_NAME"
  12.198 -    ;;
  12.199 -  macos)
  12.200 -    purge_target 'contrib -name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
  12.201 -    mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/."
  12.202 -
  12.203 -    perl -pi \
  12.204 -      -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
  12.205 -      -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
  12.206 -      -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
  12.207 -      -e "s,plugin-blacklist.MacOSX.jar=true,plugin-blacklist.MacOSX.jar=,g;" \
  12.208 -      "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
  12.209 -    ;;
  12.210 -  windows)
  12.211 -    purge_target 'contrib -name "x86*-linux" -o -name "x86*-darwin" -o -name "x86-cygwin"'
  12.212 -
  12.213 -    mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."
  12.214 -
  12.215 -    perl -pi \
  12.216 -      -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
  12.217 -      -e "s,foldPainter=.*,foldPainter=Square,g;" \
  12.218 -      "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
  12.219 -
  12.220 -    (
  12.221 -      init_component "$JEDIT_HOME"
  12.222 -
  12.223 -      echo -e "# Java runtime options\r"
  12.224 -      eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
  12.225 -      for ARG in "${JAVA_ARGS[@]}"
  12.226 -      do
  12.227 -        echo -e "$ARG\r"
  12.228 -      done
  12.229 -      echo -e "-Disabelle.jedit_server=${ISABELLE_NAME}\r"
  12.230 -    ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.l4j.ini"
  12.231 -
  12.232 -    (
  12.233 -      cd "$TMP"
  12.234 -
  12.235 -      APP_TEMPLATE="$ISABELLE_HOME/Admin/Windows/launch4j"
  12.236 -
  12.237 -      (
  12.238 -        for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
  12.239 -        do
  12.240 -          ENTRY=$(echo "$ENTRY" | perl -p -e 's,/,\\\\,g;')
  12.241 -          echo "    <cp>%EXEDIR%\\\\$ENTRY</cp>"
  12.242 -        done
  12.243 -      ) > exe_classpath
  12.244 -      EXE_CLASSPATH="$(cat exe_classpath)"
  12.245 -
  12.246 -      perl -p \
  12.247 -        -e "s,{OUTFILE},$ISABELLE_TARGET/${ISABELLE_NAME}.exe,g;" \
  12.248 -        -e "s,{ICON},$APP_TEMPLATE/isabelle_transparent.ico,g;" \
  12.249 -        -e "s,{SPLASH},$APP_TEMPLATE/isabelle.bmp,g;" \
  12.250 -        -e "s,{CLASSPATH},$EXE_CLASSPATH,g;" \
  12.251 -        -e "s,{ISABELLE_NAME},$ISABELLE_NAME,g;" \
  12.252 -        "$APP_TEMPLATE/isabelle.xml" > isabelle.xml
  12.253 -
  12.254 -      "windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j" isabelle.xml
  12.255 -
  12.256 -      cp "$APP_TEMPLATE/manifest.xml" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe.manifest"
  12.257 -    )
  12.258 -
  12.259 -    (
  12.260 -      cd "$ISABELLE_TARGET"
  12.261 -
  12.262 -      cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" .
  12.263 -
  12.264 -      CYGWIN_MIRROR="$(cat contrib/cygwin/isabelle/cygwin_mirror)"
  12.265 -      cat "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" | \
  12.266 -        perl -p > "Cygwin-Setup.bat" -e "s,{MIRROR},$CYGWIN_MIRROR,;"
  12.267 -      chmod +x "Cygwin-Setup.bat"
  12.268 -
  12.269 -      for NAME in postinstall rebaseall
  12.270 -      do
  12.271 -        cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" \
  12.272 -          "contrib/cygwin/isabelle/."
  12.273 -      done
  12.274 -
  12.275 -      if [ "$ISABELLE_PLATFORM_FAMILY" = macos ]; then
  12.276 -        find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
  12.277 -          -print0 > "contrib/cygwin/isabelle/executables"
  12.278 -      else
  12.279 -        find . -type f -not -name '*.exe' -not -name '*.dll' -executable \
  12.280 -          -print0 > "contrib/cygwin/isabelle/executables"
  12.281 -      fi
  12.282 -
  12.283 -      find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
  12.284 -        > "contrib/cygwin/isabelle/symlinks"
  12.285 -      find . -type l -exec rm "{}" ";"
  12.286 -
  12.287 -      touch "contrib/cygwin/isabelle/uninitialized"
  12.288 -    )
  12.289 -    ;;
  12.290 -  *)
  12.291 -    ;;
  12.292 -esac
  12.293 -
  12.294 -
  12.295 -# archive
  12.296 -
  12.297 -BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz"
  12.298 -
  12.299 -echo "packaging $(basename "$BUNDLE_ARCHIVE")"
  12.300 -tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" || exit 2
  12.301 -
  12.302 -
  12.303 -# platform-specific setup (outside archive)
  12.304 -
  12.305 -case "$PLATFORM_FAMILY" in
  12.306 -  linux)
  12.307 -    echo "application for $PLATFORM_FAMILY"
  12.308 -    ln -s "${ISABELLE_NAME}_linux.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}_app.tar.gz"
  12.309 -    ;;
  12.310 -  macos)
  12.311 -    echo "application for $PLATFORM_FAMILY"
  12.312 -    (
  12.313 -      cd "$TMP"
  12.314 -
  12.315 -      APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS"
  12.316 -      APP="dmg/${ISABELLE_NAME}.app"
  12.317 -
  12.318 -      mkdir -p "dmg/.background"
  12.319 -      cp "$APP_TEMPLATE/dmg/background.png" "dmg/.background/"
  12.320 -      cp "$APP_TEMPLATE/dmg/DS_Store" "dmg/.DS_Store"
  12.321 -      ln -s /Applications "dmg/."
  12.322 -
  12.323 -      for NAME in Java MacOS PlugIns Resources
  12.324 -      do
  12.325 -        mkdir -p "$APP/Contents/$NAME"
  12.326 -      done
  12.327 -
  12.328 -      (
  12.329 -        init_component "$JEDIT_HOME"
  12.330 -
  12.331 -        cat "$APP_TEMPLATE/Info.plist-part1"
  12.332 -
  12.333 -        declare -a OPTIONS=()
  12.334 -        eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
  12.335 -        for OPT in "${OPTIONS[@]}"
  12.336 -        do
  12.337 -          echo "<string>$OPT</string>"
  12.338 -        done
  12.339 -        echo "<string>-Disabelle.jedit_server={ISABELLE_NAME}</string>"
  12.340 -        echo "<string>-Dapple.awt.application.name={ISABELLE_NAME}</string>"
  12.341 -
  12.342 -        cat "$APP_TEMPLATE/Info.plist-part2"
  12.343 -      ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
  12.344 -
  12.345 -      for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
  12.346 -      do
  12.347 -        ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$APP/Contents/Java"
  12.348 -      done
  12.349 -
  12.350 -      cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
  12.351 -
  12.352 -      ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk/x86_64-darwin" \
  12.353 -        "$APP/Contents/PlugIns/bundled.jdk"
  12.354 -
  12.355 -      cp macos_app/JavaAppLauncher "$APP/Contents/MacOS/." && \
  12.356 -        chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
  12.357 -
  12.358 -      mv "$ISABELLE_NAME" "$APP/Contents/Resources/."
  12.359 -      ln -sf "../../Info.plist" "$APP/Contents/Resources/$ISABELLE_NAME/${ISABELLE_NAME}.plist"
  12.360 -      ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
  12.361 -
  12.362 -      rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
  12.363 -      tar -C dmg -czf "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" .
  12.364 -
  12.365 -      if [ -n "$REMOTE_MAC" ]
  12.366 -      then
  12.367 -        echo -n "$REMOTE_MAC: building dmg ..."
  12.368 -        isabelle remote_dmg -V Isabelle "$REMOTE_MAC" \
  12.369 -          "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" &&
  12.370 -          echo " done"
  12.371 -      fi
  12.372 -    )
  12.373 -    ;;
  12.374 -  windows)
  12.375 -    (
  12.376 -      cd "$TMP"
  12.377 -      rm -f "$TMP/${ISABELLE_NAME}.7z"
  12.378 -      7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME"
  12.379 -      [ -f "$TMP/${ISABELLE_NAME}.7z" ] || exit 2
  12.380 -
  12.381 -      echo "application for $PLATFORM_FAMILY"
  12.382 -      (
  12.383 -        cat "windows_app/7zsd_All_x64.sfx"
  12.384 -        cat "$ISABELLE_HOME/Admin/Windows/Installer/sfx.txt" | \
  12.385 -          perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;"
  12.386 -        cat "$TMP/${ISABELLE_NAME}.7z"
  12.387 -      ) > "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
  12.388 -      chmod +x "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
  12.389 -    )
  12.390 -    ;;
  12.391 -  *)
  12.392 -    ;;
  12.393 -esac
  12.394 -
  12.395 -
  12.396 -# clean up
  12.397 -rm -rf "$TMP"
    13.1 --- a/src/Pure/Admin/build_release.scala	Tue Dec 04 16:11:52 2018 +0100
    13.2 +++ b/src/Pure/Admin/build_release.scala	Wed Dec 05 19:42:40 2018 +0100
    13.3 @@ -21,6 +21,7 @@
    13.4    }
    13.5  
    13.6    class Release private[Build_Release](
    13.7 +    progress: Progress,
    13.8      val date: Date,
    13.9      val dist_name: String,
   13.10      val dist_dir: Path,
   13.11 @@ -31,7 +32,10 @@
   13.12      val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
   13.13      val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
   13.14  
   13.15 -    val other_isabelle_identifier: String = dist_name + "-build"
   13.16 +    def other_isabelle(dir: Path): Other_Isabelle =
   13.17 +      Other_Isabelle(dir + Path.explode(dist_name),
   13.18 +        isabelle_identifier = dist_name + "-build",
   13.19 +        progress = progress)
   13.20  
   13.21      def bundle_info(platform_family: String): Bundle_Info =
   13.22        platform_family match {
   13.23 @@ -168,10 +172,17 @@
   13.24          } yield bundled(line)).toList))
   13.25    }
   13.26  
   13.27 -  def get_bundled_components(dir: Path, platform: String): List[String] =
   13.28 +  def get_bundled_components(dir: Path, platform: String): (List[String], String) =
   13.29    {
   13.30      val Bundled = new Bundled(platform)
   13.31 -    for (Bundled(name) <- Components.read_components(dir)) yield name
   13.32 +    val components =
   13.33 +      for {
   13.34 +        Bundled(name) <- Components.read_components(dir)
   13.35 +        if !name.startsWith("jedit_build")
   13.36 +      } yield name
   13.37 +    val jdk_component =
   13.38 +      components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
   13.39 +    (components, jdk_component)
   13.40    }
   13.41  
   13.42    def activate_bundled_components(dir: Path, platform: String)
   13.43 @@ -202,28 +213,6 @@
   13.44  
   13.45    /** build_release **/
   13.46  
   13.47 -  def distribution_classpath(
   13.48 -    components_base: Path,
   13.49 -    isabelle_home: Path,
   13.50 -    isabelle_classpath: String): List[Path] =
   13.51 -  {
   13.52 -    val base = isabelle_home.absolute
   13.53 -    val contrib_base = components_base.absolute
   13.54 -
   13.55 -    Path.split(isabelle_classpath).map(path =>
   13.56 -    {
   13.57 -      val abs_path = path.absolute
   13.58 -      File.relative_path(base, abs_path) match {
   13.59 -        case Some(rel_path) => rel_path
   13.60 -        case None =>
   13.61 -          File.relative_path(contrib_base, abs_path) match {
   13.62 -            case Some(rel_path) => Components.contrib() + rel_path
   13.63 -            case None => error("Bad ISABELLE_CLASSPATH element: " + path)
   13.64 -          }
   13.65 -      }
   13.66 -    }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
   13.67 -  }
   13.68 -
   13.69    private def execute(dir: Path, script: String): Unit =
   13.70      Isabelle_System.bash(script, cwd = dir.file).check
   13.71  
   13.72 @@ -236,6 +225,7 @@
   13.73    private val default_platform_families = List("linux", "windows", "macos")
   13.74  
   13.75    def build_release(base_dir: Path,
   13.76 +    options: Options,
   13.77      components_base: Option[Path] = None,
   13.78      progress: Progress = No_Progress,
   13.79      rev: String = "",
   13.80 @@ -267,7 +257,7 @@
   13.81            case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
   13.82          }
   13.83  
   13.84 -      new Release(date, dist_name, dist_dir, dist_version, ident)
   13.85 +      new Release(progress, date, dist_name, dist_dir, dist_version, ident)
   13.86      }
   13.87  
   13.88  
   13.89 @@ -320,13 +310,12 @@
   13.90  
   13.91        execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
   13.92  
   13.93 +      record_bundled_components(release.isabelle_dir)
   13.94 +
   13.95  
   13.96        /* build tools and documentation */
   13.97  
   13.98 -      val other_isabelle =
   13.99 -        Other_Isabelle(release.isabelle_dir,
  13.100 -          isabelle_identifier = release.other_isabelle_identifier,
  13.101 -          progress = progress)
  13.102 +      val other_isabelle = release.other_isabelle(release.dist_dir)
  13.103  
  13.104        other_isabelle.init_settings(
  13.105          other_isabelle.init_components(base = components_base, catalogs = List("main")))
  13.106 @@ -406,13 +395,262 @@
  13.107        if (bundle_archive.is_file)
  13.108          progress.echo_warning("Application bundle already exists: " + bundle_archive)
  13.109        else {
  13.110 -        progress.echo(
  13.111 -          "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive)
  13.112 -        progress.bash(
  13.113 -          "isabelle makedist_bundle " + File.bash_path(release.isabelle_archive) +
  13.114 -            " " + Bash.string(bundle_info.platform_family) +
  13.115 -            (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
  13.116 -          echo = true).check
  13.117 +        val isabelle_name = release.dist_name
  13.118 +        val platform = bundle_info.platform_family
  13.119 +
  13.120 +        progress.echo("\nApplication bundle for " + platform + ": " + bundle_archive)
  13.121 +
  13.122 +        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
  13.123 +        {
  13.124 +          // release archive
  13.125 +
  13.126 +          execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
  13.127 +          val other_isabelle = release.other_isabelle(tmp_dir)
  13.128 +          val isabelle_target = other_isabelle.isabelle_home
  13.129 +
  13.130 +
  13.131 +          // bundled components
  13.132 +
  13.133 +          progress.echo("Bundled components:")
  13.134 +
  13.135 +          val contrib_dir = Components.contrib(isabelle_target)
  13.136 +
  13.137 +          val (components, jdk_component) = get_bundled_components(isabelle_target, platform)
  13.138 +
  13.139 +          Components.resolve(other_isabelle.components_base(components_base),
  13.140 +            components, target_dir = Some(contrib_dir), progress = progress)
  13.141 +
  13.142 +          Components.purge(contrib_dir, platform)
  13.143 +
  13.144 +          activate_bundled_components(isabelle_target, platform)
  13.145 +
  13.146 +
  13.147 +          // Java parameters
  13.148 +
  13.149 +          val java_options_title = "# Java runtime options"
  13.150 +          val java_options: List[String] =
  13.151 +            (for {
  13.152 +              variable <-
  13.153 +                List(
  13.154 +                  "ISABELLE_JAVA_SYSTEM_OPTIONS",
  13.155 +                  "JEDIT_JAVA_SYSTEM_OPTIONS",
  13.156 +                  "JEDIT_JAVA_OPTIONS")
  13.157 +              opt <- Word.explode(other_isabelle.getenv(variable))
  13.158 +            } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
  13.159 +
  13.160 +          val classpath: List[Path] =
  13.161 +          {
  13.162 +            val base = isabelle_target.absolute
  13.163 +            Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
  13.164 +            {
  13.165 +              val abs_path = path.absolute
  13.166 +              File.relative_path(base, abs_path) match {
  13.167 +                case Some(rel_path) => rel_path
  13.168 +                case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
  13.169 +              }
  13.170 +            }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
  13.171 +          }
  13.172 +
  13.173 +          val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
  13.174 +
  13.175 +
  13.176 +          // platform-specific setup (inside archive)
  13.177 +
  13.178 +          if (platform == "linux") {
  13.179 +            File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
  13.180 +              terminate_lines(java_options_title :: java_options))
  13.181 +
  13.182 +            val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
  13.183 +            File.write(isabelle_run,
  13.184 +              File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
  13.185 +                .replaceAllLiterally("{CLASSPATH}",
  13.186 +                  classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
  13.187 +                .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
  13.188 +            Isabelle_System.bash("chmod +x " + File.bash_path(isabelle_run)).check
  13.189 +
  13.190 +            val linux_app = isabelle_target + Path.explode("contrib/linux_app")
  13.191 +            File.move(linux_app + Path.explode("Isabelle"),
  13.192 +              isabelle_target + Path.explode(isabelle_name))
  13.193 +            Isabelle_System.rm_tree(linux_app)
  13.194 +          }
  13.195 +          else if (platform == "macos") {
  13.196 +            File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
  13.197 +            File.write(isabelle_target + jedit_props,
  13.198 +              File.read(isabelle_target + jedit_props)
  13.199 +                .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
  13.200 +                .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
  13.201 +                .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
  13.202 +                .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
  13.203 +          }
  13.204 +          else if (platform == "windows") {
  13.205 +            val app_template = Path.explode("~~/Admin/Windows/launch4j")
  13.206 +            val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
  13.207 +
  13.208 +            File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
  13.209 +
  13.210 +            File.write(isabelle_target + jedit_props,
  13.211 +              File.read(isabelle_target + jedit_props)
  13.212 +                .replaceAll("lookAndFeel=.*",
  13.213 +                  "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
  13.214 +                .replaceAll("foldPainter=.*", "foldPainter=Square"))
  13.215 +
  13.216 +            File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
  13.217 +              (java_options_title :: java_options).map(_ + "\r\n").mkString)
  13.218 +
  13.219 +            val isabelle_xml = Path.explode("isabelle.xml")
  13.220 +            val isabelle_exe = Path.explode(isabelle_name + ".exe")
  13.221 +
  13.222 +            File.write(tmp_dir + isabelle_xml,
  13.223 +              File.read(app_template + isabelle_xml)
  13.224 +                .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
  13.225 +                .replaceAllLiterally("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
  13.226 +                .replaceAllLiterally("{ICON}",
  13.227 +                  File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
  13.228 +                .replaceAllLiterally("{SPLASH}",
  13.229 +                  File.platform_path(app_template + Path.explode("isabelle.bmp")))
  13.230 +                .replaceAllLiterally("{CLASSPATH}",
  13.231 +                  cat_lines(classpath.map(cp =>
  13.232 +                    "    <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
  13.233 +                .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
  13.234 +
  13.235 +            Isabelle_System.bash(
  13.236 +              "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml",
  13.237 +              cwd = tmp_dir.file).check
  13.238 +
  13.239 +            File.copy(app_template + Path.explode("manifest.xml"),
  13.240 +              isabelle_target + isabelle_exe.ext("manifest"))
  13.241 +
  13.242 +
  13.243 +            File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
  13.244 +
  13.245 +            val cygwin_mirror =
  13.246 +              File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
  13.247 +
  13.248 +            val cygwin_bat = Path.explode("Cygwin-Setup.bat")
  13.249 +            File.write(isabelle_target + cygwin_bat,
  13.250 +              File.read(cygwin_template + cygwin_bat)
  13.251 +                .replaceAllLiterally("{MIRROR}", cygwin_mirror))
  13.252 +
  13.253 +            Isabelle_System.bash("chmod +x " + File.bash_path(isabelle_target + cygwin_bat)).check
  13.254 +
  13.255 +            for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
  13.256 +              val path = Path.explode(name)
  13.257 +              File.copy(cygwin_template + path,
  13.258 +                isabelle_target + Path.explode("contrib/cygwin") + path)
  13.259 +            }
  13.260 +
  13.261 +            Isabelle_System.bash("""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
  13.262 +              (if (Platform.is_macos) "-perm +100" else "-executable") +
  13.263 +              " -print0 > contrib/cygwin/isabelle/executables",
  13.264 +              cwd = isabelle_target.file).check
  13.265 +
  13.266 +            Isabelle_System.bash("""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
  13.267 +              """> contrib/cygwin/isabelle/symlinks""",
  13.268 +              cwd = isabelle_target.file).check
  13.269 +
  13.270 +            Isabelle_System.bash("""find . -type l -exec rm "{}" ";" """,
  13.271 +              cwd = isabelle_target.file).check
  13.272 +
  13.273 +            File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
  13.274 +          }
  13.275 +
  13.276 +
  13.277 +          // archive
  13.278 +
  13.279 +          val archive_name = isabelle_name + "_" + platform + ".tar.gz"
  13.280 +          progress.echo("Packaging " + archive_name)
  13.281 +          execute_tar(tmp_dir,
  13.282 +            "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
  13.283 +            Bash.string(isabelle_name))
  13.284 +
  13.285 +
  13.286 +          // platform-specific application (outside archive)
  13.287 +
  13.288 +          progress.echo("Application for " + platform)
  13.289 +
  13.290 +          if (platform == "linux") {
  13.291 +            Isabelle_System.bash(
  13.292 +              "ln -s " + Bash.string(isabelle_name + "_linux.tar.gz") + " " +
  13.293 +              File.bash_path(release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"))).check
  13.294 +          }
  13.295 +          else if (platform == "macos") {
  13.296 +            val dmg_dir = tmp_dir + Path.explode("macos_app/dmg")
  13.297 +            val app_dir = dmg_dir + Path.explode(isabelle_name + ".app")
  13.298 +            File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir)
  13.299 +
  13.300 +            val app_contents = app_dir + Path.explode("Contents")
  13.301 +            val app_resources = app_contents + Path.explode("Resources")
  13.302 +            File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
  13.303 +
  13.304 +            File.write(app_contents + Path.explode("Info.plist"),
  13.305 +              File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
  13.306 +                .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
  13.307 +                .replaceAllLiterally("{JAVA_OPTIONS}",
  13.308 +                  terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
  13.309 +
  13.310 +            for (cp <- classpath) {
  13.311 +              Isabelle_System.bash(
  13.312 +                "ln -sf " +
  13.313 +                Bash.string("../Resources/" + isabelle_name + "/") + File.bash_path(cp) + " " +
  13.314 +                File.bash_path(app_contents + Path.explode("Java"))).check
  13.315 +            }
  13.316 +
  13.317 +            Isabelle_System.bash("ln -sf ../Resources/" + Bash.string(isabelle_name) +
  13.318 +              "/contrib/" + Bash.string(jdk_component) + "/x86_64-darwin " +
  13.319 +              File.bash_path(app_contents + Path.explode("PlugIns/bundled.jdk"))).check
  13.320 +
  13.321 +            Isabelle_System.bash("ln -sf ../../Info.plist " +
  13.322 +              File.bash_path(app_resources + Path.explode(isabelle_name) +
  13.323 +                Path.explode(isabelle_name + ".plist"))).check
  13.324 +            Isabelle_System.bash("ln -sf Contents/Resources/" + Bash.string(isabelle_name) + " " +
  13.325 +              File.bash_path(app_dir) + "/Isabelle").check
  13.326 +
  13.327 +            val dmg = Path.explode(isabelle_name + ".dmg")
  13.328 +            (release.dist_dir + dmg).file.delete
  13.329 +
  13.330 +            val dmg_archive = Path.explode(isabelle_name + "_dmg.tar.gz")
  13.331 +            execute_tar(dmg_dir, "-czf " + File.bash_path(release.dist_dir + dmg_archive) + " .")
  13.332 +
  13.333 +            remote_mac match {
  13.334 +              case SSH.Target(user, host) =>
  13.335 +                progress.echo("Building dmg on " + quote(host) + " ...")
  13.336 +                using(SSH.open_session(options, host = host, user = user))(ssh =>
  13.337 +                {
  13.338 +                  ssh.with_tmp_dir(remote_dir =>
  13.339 +                  {
  13.340 +                    val cd = "cd " + ssh.bash_path(remote_dir) + "; "
  13.341 +                    ssh.write_file(remote_dir + dmg_archive, release.dist_dir + dmg_archive)
  13.342 +                    ssh.execute(
  13.343 +                      cd + "mkdir root && tar -C root -xzf " + ssh.bash_path(dmg_archive)).check
  13.344 +                    ssh.execute(
  13.345 +                      cd + "hdiutil create -srcfolder root -volname Isabelle " +
  13.346 +                      ssh.bash_path(dmg)).check
  13.347 +                    ssh.read_file(remote_dir + dmg, release.dist_dir + dmg)
  13.348 +                  })
  13.349 +                })
  13.350 +              case _ =>
  13.351 +            }
  13.352 +          }
  13.353 +          else if (platform == "windows") {
  13.354 +            val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z")
  13.355 +            exe_archive.file.delete
  13.356 +
  13.357 +            Isabelle_System.bash("7z -y -bd a " + File.bash_path(exe_archive) + " " +
  13.358 +              Bash.string(isabelle_name), cwd = tmp_dir.file).check
  13.359 +            if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
  13.360 +
  13.361 +            val isabelle_exe = Path.explode(isabelle_name + ".exe")
  13.362 +            val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
  13.363 +            val sfx_txt =
  13.364 +              File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
  13.365 +                replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
  13.366 +
  13.367 +            Bytes.write(release.dist_dir + isabelle_exe,
  13.368 +              Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
  13.369 +
  13.370 +            Isabelle_System.bash("chmod +x " + (release.dist_dir + isabelle_exe)).check
  13.371 +          }
  13.372 +        })
  13.373        }
  13.374      }
  13.375  
  13.376 @@ -452,14 +690,12 @@
  13.377        else {
  13.378          Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
  13.379            {
  13.380 -            val name = release.dist_name
  13.381              val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
  13.382 -            val bundle = release.dist_dir + Path.explode(name + "_" + platform + ".tar.gz")
  13.383 +            val bundle =
  13.384 +              release.dist_dir + Path.explode(release.dist_name + "_" + platform + ".tar.gz")
  13.385              execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
  13.386  
  13.387 -            val other_isabelle =
  13.388 -              Other_Isabelle(tmp_dir + Path.explode(name),
  13.389 -                isabelle_identifier = release.other_isabelle_identifier, progress = progress)
  13.390 +            val other_isabelle = release.other_isabelle(tmp_dir)
  13.391  
  13.392              Isabelle_System.mkdirs(other_isabelle.etc)
  13.393              File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
  13.394 @@ -469,11 +705,11 @@
  13.395                  " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
  13.396              other_isabelle.isabelle_home_user.file.delete
  13.397  
  13.398 -            execute(tmp_dir, "chmod -R a+r " + Bash.string(name))
  13.399 -            execute(tmp_dir, "chmod -R g=o " + Bash.string(name))
  13.400 +            execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
  13.401 +            execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
  13.402              execute_tar(tmp_dir,
  13.403                tar_options + " -czf " + File.bash_path(release.isabelle_library_archive) +
  13.404 -              " " + Bash.string(name + "/browser_info"))
  13.405 +              " " + Bash.string(release.dist_name + "/browser_info"))
  13.406            })
  13.407        }
  13.408      }
  13.409 @@ -496,6 +732,7 @@
  13.410        var website: Option[Path] = None
  13.411        var parallel_jobs = 1
  13.412        var build_library = false
  13.413 +      var options = Options.init()
  13.414        var platform_families = default_platform_families
  13.415        var rev = ""
  13.416  
  13.417 @@ -511,6 +748,7 @@
  13.418      -W WEBSITE   produce minimal website in given directory
  13.419      -j INT       maximum number of parallel jobs (default 1)
  13.420      -l           build library
  13.421 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
  13.422      -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
  13.423      -r REV       Mercurial changeset id (default: RELEASE or tip)
  13.424  
  13.425 @@ -524,6 +762,7 @@
  13.426          "W:" -> (arg => website = Some(Path.explode(arg))),
  13.427          "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
  13.428          "l" -> (_ => build_library = true),
  13.429 +        "o:" -> (arg => options = options + arg),
  13.430          "p:" -> (arg => platform_families = space_explode(',', arg)),
  13.431          "r:" -> (arg => rev = arg))
  13.432  
  13.433 @@ -532,8 +771,8 @@
  13.434  
  13.435        val progress = new Console_Progress()
  13.436  
  13.437 -      build_release(Path.explode(base_dir), components_base = components_base, progress = progress,
  13.438 -        rev = rev, afp_rev = afp_rev, official_release = official_release,
  13.439 +      build_release(Path.explode(base_dir), options, components_base = components_base,
  13.440 +        progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
  13.441          proper_release_name = proper_release_name, website = website,
  13.442          platform_families =
  13.443            if (platform_families.isEmpty) default_platform_families
    14.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Dec 04 16:11:52 2018 +0100
    14.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Dec 05 19:42:40 2018 +0100
    14.3 @@ -75,7 +75,7 @@
    14.4    val build_release =
    14.5      Logger_Task("build_release", logger =>
    14.6        {
    14.7 -        Isabelle_Devel.release_snapshot(
    14.8 +        Isabelle_Devel.release_snapshot(logger.options,
    14.9            rev = get_rev(), afp_rev = get_afp_rev(), remote_mac = "macbroy30")
   14.10        })
   14.11  
    15.1 --- a/src/Pure/Admin/isabelle_devel.scala	Tue Dec 04 16:11:52 2018 +0100
    15.2 +++ b/src/Pure/Admin/isabelle_devel.scala	Wed Dec 05 19:42:40 2018 +0100
    15.3 @@ -51,6 +51,7 @@
    15.4    /* release snapshot */
    15.5  
    15.6    def release_snapshot(
    15.7 +    options: Options,
    15.8      rev: String = "",
    15.9      afp_rev: String = "",
   15.10      parallel_jobs: Int = 1,
   15.11 @@ -60,7 +61,7 @@
   15.12        {
   15.13          Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
   15.14            website_dir =>
   15.15 -            Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
   15.16 +            Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev,
   15.17                parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir)))
   15.18        })
   15.19    }
    16.1 --- a/src/Pure/Admin/other_isabelle.scala	Tue Dec 04 16:11:52 2018 +0100
    16.2 +++ b/src/Pure/Admin/other_isabelle.scala	Wed Dec 05 19:42:40 2018 +0100
    16.3 @@ -68,12 +68,15 @@
    16.4  
    16.5    /* components */
    16.6  
    16.7 +  def components_base(base: Option[Path]): Path =
    16.8 +    base getOrElse Components.contrib(isabelle_home_user.absolute.dir)
    16.9 +
   16.10    def init_components(
   16.11      base: Option[Path] = None,
   16.12      catalogs: List[String] = Nil,
   16.13      components: List[String] = Nil): List[String] =
   16.14    {
   16.15 -    val base_dir = base getOrElse Components.contrib(isabelle_home_user.absolute.dir)
   16.16 +    val base_dir = components_base(base)
   16.17      val dir = Components.admin(isabelle_home.absolute)
   16.18      catalogs.map(name =>
   16.19        "init_components " + File.bash_path(base_dir) + " " + File.bash_path(dir + Path.basic(name))) :::
    17.1 --- a/src/Pure/Admin/remote_dmg.scala	Tue Dec 04 16:11:52 2018 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,64 +0,0 @@
    17.4 -/*  Title:      Pure/Admin/remote_dmg.scala
    17.5 -    Author:     Makarius
    17.6 -
    17.7 -Build dmg on remote Mac OS X system.
    17.8 -*/
    17.9 -
   17.10 -package isabelle
   17.11 -
   17.12 -
   17.13 -object Remote_DMG
   17.14 -{
   17.15 -  def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
   17.16 -  {
   17.17 -    ssh.with_tmp_dir(remote_dir =>
   17.18 -      {
   17.19 -        val cd = "cd " + ssh.bash_path(remote_dir) + "; "
   17.20 -
   17.21 -        ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
   17.22 -        ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
   17.23 -        ssh.execute(
   17.24 -          cd + "hdiutil create -srcfolder root" +
   17.25 -            (if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) +
   17.26 -            " dmg.dmg").check
   17.27 -        ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
   17.28 -      })
   17.29 -  }
   17.30 -
   17.31 -
   17.32 -  /* Isabelle tool wrapper */
   17.33 -
   17.34 -  val isabelle_tool =
   17.35 -    Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
   17.36 -    {
   17.37 -      Command_Line.tool0 {
   17.38 -        var port = 0
   17.39 -        var volume_name = ""
   17.40 -
   17.41 -        val getopts = Getopts("""
   17.42 -Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
   17.43 -
   17.44 -  Options are:
   17.45 -    -p PORT      alternative SSH port
   17.46 -    -V NAME      specify volume name
   17.47 -
   17.48 -  Turn the contents of a tar.gz file into a dmg file -- produced on a remote
   17.49 -  Mac OS X system.
   17.50 -""",
   17.51 -          "p:" -> (arg => port = Value.Int.parse(arg)),
   17.52 -          "V:" -> (arg => volume_name = arg))
   17.53 -
   17.54 -        val more_args = getopts(args)
   17.55 -        val (user, host, tar_gz_file, dmg_file) =
   17.56 -          more_args match {
   17.57 -            case List(SSH.Target(user, host), tar_gz_file, dmg_file) =>
   17.58 -              (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
   17.59 -            case _ => getopts.usage()
   17.60 -          }
   17.61 -
   17.62 -        val options = Options.init()
   17.63 -        using(SSH.open_session(options, host = host, user = user, port = port))(
   17.64 -          remote_dmg(_, tar_gz_file, dmg_file, volume_name))
   17.65 -      }
   17.66 -    })
   17.67 -}
    18.1 --- a/src/Pure/System/components.scala	Tue Dec 04 16:11:52 2018 +0100
    18.2 +++ b/src/Pure/System/components.scala	Wed Dec 05 19:42:40 2018 +0100
    18.3 @@ -7,6 +7,9 @@
    18.4  package isabelle
    18.5  
    18.6  
    18.7 +import java.io.{File => JFile}
    18.8 +
    18.9 +
   18.10  object Components
   18.11  {
   18.12    /* component collections */
   18.13 @@ -16,20 +19,43 @@
   18.14    def contrib(dir: Path = Path.current, name: String = ""): Path =
   18.15      dir + Path.explode("contrib") + Path.explode(name)
   18.16  
   18.17 -  def download(dir: Path, names: List[String], progress: Progress = No_Progress)
   18.18 +  def resolve(base_dir: Path, names: List[String],
   18.19 +    target_dir: Option[Path] = None,
   18.20 +    progress: Progress = No_Progress)
   18.21    {
   18.22 -    Isabelle_System.mkdirs(dir)
   18.23 +    Isabelle_System.mkdirs(base_dir)
   18.24      for (name <- names) {
   18.25 -      val archive = name + ".tar.gz"
   18.26 -      val target = dir + Path.explode(archive)
   18.27 -      if (!target.is_file) {
   18.28 -        val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive
   18.29 -        progress.echo("Getting " + quote(remote))
   18.30 -        Bytes.write(target, Url.read_bytes(Url(remote)))
   18.31 +      val archive_name = name + ".tar.gz"
   18.32 +      val archive = base_dir + Path.explode(archive_name)
   18.33 +      if (!archive.is_file) {
   18.34 +        val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
   18.35 +        progress.echo("Getting " + remote)
   18.36 +        Bytes.write(archive, Url.read_bytes(Url(remote)))
   18.37        }
   18.38 +      progress.echo("Unpacking " + archive_name)
   18.39 +      Isabelle_System.gnutar(
   18.40 +        "-C " + File.bash_path(target_dir getOrElse base_dir) +
   18.41 +        " -xzf " + File.bash_path(archive)).check
   18.42      }
   18.43    }
   18.44  
   18.45 +  def purge(dir: Path, platform: String)
   18.46 +  {
   18.47 +    def purge_platforms(platforms: String*): Set[String] =
   18.48 +      platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
   18.49 +    val purge_set =
   18.50 +      platform match {
   18.51 +        case "linux" => purge_platforms("darwin", "cygwin", "windows")
   18.52 +        case "windows" => purge_platforms("linux", "darwin")
   18.53 +        case "macos" => purge_platforms("linux", "cygwin", "windows")
   18.54 +        case _ => error("Bad platform: " + quote(platform))
   18.55 +      }
   18.56 +
   18.57 +    File.find_files(dir.file,
   18.58 +      (file: JFile) => file.isDirectory && purge_set(file.getName),
   18.59 +      include_dirs = true).foreach(Isabelle_System.rm_tree)
   18.60 +  }
   18.61 +
   18.62  
   18.63    /* component directory content */
   18.64  
    19.1 --- a/src/Pure/System/isabelle_tool.scala	Tue Dec 04 16:11:52 2018 +0100
    19.2 +++ b/src/Pure/System/isabelle_tool.scala	Wed Dec 05 19:42:40 2018 +0100
    19.3 @@ -172,5 +172,4 @@
    19.4    Build_PolyML.isabelle_tool2,
    19.5    Build_Status.isabelle_tool,
    19.6    Check_Sources.isabelle_tool,
    19.7 -  Remote_DMG.isabelle_tool,
    19.8    isabelle.vscode.Build_VSCode.isabelle_tool)
    20.1 --- a/src/Pure/build-jars	Tue Dec 04 16:11:52 2018 +0100
    20.2 +++ b/src/Pure/build-jars	Wed Dec 05 19:42:40 2018 +0100
    20.3 @@ -25,7 +25,6 @@
    20.4    Admin/isabelle_devel.scala
    20.5    Admin/jenkins.scala
    20.6    Admin/other_isabelle.scala
    20.7 -  Admin/remote_dmg.scala
    20.8    Concurrent/consumer_thread.scala
    20.9    Concurrent/counter.scala
   20.10    Concurrent/event_timer.scala