eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
authorwenzelm
Wed, 05 Dec 2018 19:42:40 +0100
changeset 69401 7a1b7b737c02
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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/Info.plist	Wed Dec 05 19:42:40 2018 +0100
@@ -0,0 +1,69 @@
+<?xml version="1.0" ?>
+<!DOCTYPE plist PUBLIC "-//Apple//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>JavaAppLauncher</string>
+<key>CFBundleIconFile</key>
+<string>isabelle.icns</string>
+<key>CFBundleIdentifier</key>
+<string>de.tum.in.isabelle.{ISABELLE_NAME}</string>
+<key>CFBundleDisplayName</key>
+<string>{ISABELLE_NAME}</string>
+<key>CFBundleInfoDictionaryVersion</key>
+<string>6.0</string>
+<key>CFBundleName</key>
+<string>{ISABELLE_NAME}</string>
+<key>CFBundlePackageType</key>
+<string>APPL</string>
+<key>CFBundleShortVersionString</key>
+<string>1.0</string>
+<key>CFBundleSignature</key>
+<string>????</string>
+<key>CFBundleVersion</key>
+<string>1</string>
+<key>NSHumanReadableCopyright</key>
+<string></string>
+<key>LSMinimumSystemVersion</key>
+<string>10.7</string>
+<key>LSApplicationCategoryType</key>
+<string>public.app-category.developer-tools</string>
+<key>NSHighResolutionCapable</key>
+<string>true</string>
+<key>NSSupportsAutomaticGraphicsSwitching</key>
+<string>true</string>
+<key>JVMRuntime</key>
+<string>bundled.jdk</string>
+<key>JVMMainClassName</key>
+<string>isabelle.Main</string>
+<key>CFBundleDocumentTypes</key>
+<array>
+<dict>
+<key>CFBundleTypeExtensions</key>
+<array>
+<string>thy</string>
+</array>
+<key>CFBundleTypeIconFile</key>
+<string>theory.icns</string>
+<key>CFBundleTypeName</key>
+<string>Isabelle theory file</string>
+<key>CFBundleTypeRole</key>
+<string>Editor</string>
+<key>LSTypeIsPackage</key>
+<false/>
+</dict>
+</array>
+<key>JVMOptions</key>
+<array>
+{JAVA_OPTIONS}
+<string>-Dapple.awt.application.name={ISABELLE_NAME}</string>
+<string>-Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
+<string>-Disabelle.app=true</string>
+</array>
+<key>JVMArguments</key>
+<array>
+</array>
+</dict>
+</plist>
--- a/Admin/MacOS/Info.plist-part1	Tue Dec 04 16:11:52 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-<?xml version="1.0" ?>
-<!DOCTYPE plist PUBLIC "-//Apple//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>JavaAppLauncher</string>
-<key>CFBundleIconFile</key>
-<string>isabelle.icns</string>
-<key>CFBundleIdentifier</key>
-<string>de.tum.in.isabelle.{ISABELLE_NAME}</string>
-<key>CFBundleDisplayName</key>
-<string>{ISABELLE_NAME}</string>
-<key>CFBundleInfoDictionaryVersion</key>
-<string>6.0</string>
-<key>CFBundleName</key>
-<string>{ISABELLE_NAME}</string>
-<key>CFBundlePackageType</key>
-<string>APPL</string>
-<key>CFBundleShortVersionString</key>
-<string>1.0</string>
-<key>CFBundleSignature</key>
-<string>????</string>
-<key>CFBundleVersion</key>
-<string>1</string>
-<key>NSHumanReadableCopyright</key>
-<string></string>
-<key>LSMinimumSystemVersion</key>
-<string>10.7</string>
-<key>LSApplicationCategoryType</key>
-<string>public.app-category.developer-tools</string>
-<key>NSHighResolutionCapable</key>
-<string>true</string>
-<key>NSSupportsAutomaticGraphicsSwitching</key>
-<string>true</string>
-<key>JVMRuntime</key>
-<string>bundled.jdk</string>
-<key>JVMMainClassName</key>
-<string>isabelle.Main</string>
-<key>CFBundleDocumentTypes</key>
-<array>
-<dict>
-<key>CFBundleTypeExtensions</key>
-<array>
-<string>thy</string>
-</array>
-<key>CFBundleTypeIconFile</key>
-<string>theory.icns</string>
-<key>CFBundleTypeName</key>
-<string>Isabelle theory file</string>
-<key>CFBundleTypeRole</key>
-<string>Editor</string>
-<key>LSTypeIsPackage</key>
-<false/>
-</dict>
-</array>
-<key>JVMOptions</key>
-<array>
--- a/Admin/MacOS/Info.plist-part2	Tue Dec 04 16:11:52 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-<string>-Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
-<string>-Disabelle.app=true</string>
-</array>
-<key>JVMArguments</key>
-<array>
-</array>
-</dict>
-</plist>
--- a/Admin/MacOS/README	Tue Dec 04 16:11:52 2018 +0100
+++ b/Admin/MacOS/README	Wed Dec 05 19:42:40 2018 +0100
@@ -5,4 +5,3 @@
 
   see appbundler-1.0.jar
   see com/oracle/appbundler/JavaAppLauncher
-
--- a/Admin/MacOS/Resources/en.lproj/Localizable.strings	Tue Dec 04 16:11:52 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-"JRELoadError" = "Unable to load Java Runtime Environment.";
-"MainClassNameRequired" = "Main class name is required.";
-"JavaDirectoryNotFound" = "Unable to enumerate Java directory contents.";
Binary file Admin/MacOS/Resources/isabelle.icns has changed
Binary file Admin/MacOS/Resources/theory.icns has changed
Binary file Admin/MacOS/dmg/DS_Store has changed
Binary file Admin/MacOS/dmg/background.png has changed
--- a/Admin/components/bundled-macos	Tue Dec 04 16:11:52 2018 +0100
+++ b/Admin/components/bundled-macos	Wed Dec 05 19:42:40 2018 +0100
@@ -1,2 +1,2 @@
 #additional components to be bundled for release
-macos_app-20130716
+macos_app-20181205
--- a/Admin/components/components.sha1	Tue Dec 04 16:11:52 2018 +0100
+++ b/Admin/components/components.sha1	Wed Dec 05 19:42:40 2018 +0100
@@ -151,6 +151,7 @@
 377e36efb8608e6c828c7718d890e97fde2006a4  linux_app-20131007.tar.gz
 0aab4f73ff7f5e36f33276547e10897e1e56fb1d  macos_app-20130716.tar.gz
 ad5d0e640ce3609a885cecab645389a2204e03bb  macos_app-20150916.tar.gz
+400af57ec5cd51f96928d9de00d077524a6fe316  macos_app-20181205.tar.gz
 26df569cee9c2fd91b9ac06714afd43f3b37a1dd  nunchaku-0.3.tar.gz
 e573f2cbb57eb7b813ed5908753cfe2cb41033ca  nunchaku-0.5.tar.gz
 fe57793aca175336deea4f5e9c0d949a197850ac  opam-1.2.2.tar.gz
--- a/Admin/lib/Tools/makedist_bundle	Tue Dec 04 16:11:52 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,394 +0,0 @@
-#!/usr/bin/env bash
-#
-# DESCRIPTION: re-package Isabelle distribution with add-on components
-
-## diagnostics
-
-PRG=$(basename "$0")
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG ARCHIVE PLATFORM_FAMILY [REMOTE_MAC]"
-  echo
-  echo "  Re-package Isabelle source distribution with add-on components and"
-  echo "  post-hoc patches for platform family linux, windows, macos."
-  echo
-  echo "  The optional remote Mac OS X system is used for dmg build."
-  echo
-  echo "  Add-on components are that of the running Isabelle version!"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## arguments
-
-[ "$#" -ne 2 -a "$#" -ne 3 ] && usage
-
-ARCHIVE="$1"; shift
-PLATFORM_FAMILY="$1"; shift
-REMOTE_MAC="$1"; shift
-
-[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
-
-ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
-ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
-
-
-## main
-
-#GNU tar (notably on Mac OS X)
-type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
-
-TMP="/var/tmp/isabelle-makedist$$"
-mkdir "$TMP" || fail "Cannot create directory $TMP"
-
-ISABELLE_TARGET="$TMP/$ISABELLE_NAME"
-
-tar -C "$TMP" -x -z -f "$ARCHIVE" || exit 2
-
-
-# distribution classpath (based on educated guesses)
-
-splitarray ":" "$ISABELLE_CLASSPATH"; CLASSPATH_ENTRIES=("${SPLITARRAY[@]}")
-declare -a DISTRIBUTION_CLASSPATH=()
-
-for ENTRY in "${CLASSPATH_ENTRIES[@]}"
-do
-  ENTRY=$(echo "$ENTRY" | perl -n -e "
-    if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; }
-    elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; }
-    elsif (m,/home/isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; }
-    else { print; };
-    print qq{\n};")
-  DISTRIBUTION_CLASSPATH["${#DISTRIBUTION_CLASSPATH[@]}"]="$ENTRY"
-done
-
-DISTRIBUTION_CLASSPATH["${#DISTRIBUTION_CLASSPATH[@]}"]="src/Tools/jEdit/dist/jedit.jar"
-
-echo "classpath"
-for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
-do
-  echo "  $ENTRY"
-done
-
-
-# bundled components
-
-if [ ! -e "$ARCHIVE_DIR/contrib" ]; then
-  if [ ! -e "$ARCHIVE_DIR/../contrib" ]; then
-    mkdir -p "$ARCHIVE_DIR/contrib"
-  else
-    ln -s "../contrib" "$ARCHIVE_DIR/contrib"
-  fi
-fi
-
-echo "#bundled components" >> "$ISABELLE_TARGET/etc/components"
-
-for CATALOG in main "$PLATFORM_FAMILY" bundled "bundled-$PLATFORM_FAMILY"
-do
-  CATALOG_FILE="$ISABELLE_HOME/Admin/components/$CATALOG"
-  if [ -f "$CATALOG_FILE" ]
-  then
-    echo "catalog ${CATALOG}"
-    {
-      while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
-      do
-        case "$REPLY" in
-          \#* | "") ;;
-          *)
-            COMPONENT="$REPLY"
-            COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
-            case "$COMPONENT" in
-              jedit_build*) ;;
-              *)
-                echo "  component $COMPONENT"
-                CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"
-                if [ ! -f "$CONTRIB" ]; then
-                  type -p curl  > /dev/null || fail "Cannot download files: missing curl"
-                  REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz"
-                  echo "  downloading $REMOTE"
-                  curl --fail --silent "$REMOTE" > "$CONTRIB" || \
-                    fail "Failed to download \"$REMOTE\""
-                  perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2
-                fi
-
-                tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB" || exit 2
-                if [ -f "$COMPONENT_DIR/etc/settings" -o -f "$COMPONENT_DIR/etc/components" ]
-                then
-                  case "$COMPONENT" in
-                    jdk-*)
-                      mv "$ISABELLE_TARGET/contrib/$COMPONENT" "$ISABELLE_TARGET/contrib/jdk"
-                      echo "contrib/jdk" >> "$ISABELLE_TARGET/etc/components"
-                      ;;
-                    *)
-                      echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
-                      ;;
-                  esac
-                fi
-                ;;
-            esac
-            ;;
-        esac
-      done
-    } < "$CATALOG_FILE"
-  fi
-done
-
-
-# purge other platforms
-
-function purge_target
-{
-  (
-    cd "$ISABELLE_TARGET"
-    for DIR in $(eval find "$@" | sort)
-    do
-      echo "removing $DIR"
-      rm -rf "$DIR"
-    done
-  )
-}
-
-
-# platform-specific setup (inside archive)
-
-case "$PLATFORM_FAMILY" in
-  linux)
-    purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
-
-    (
-      init_component "$JEDIT_HOME"
-
-      echo "# Java runtime options"
-      eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
-      for ARG in "${JAVA_ARGS[@]}"
-      do
-        echo "$ARG"
-      done
-      echo "-Disabelle.jedit_server=${ISABELLE_NAME}"
-    ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.options"
-
-    LINUX_CLASSPATH=""
-    for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
-    do
-      if [ -z "$LINUX_CLASSPATH" ]; then
-        LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY"
-      else
-        LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY"
-      fi
-    done
-
-    cat "$ISABELLE_HOME/Admin/Linux/Isabelle.run" | \
-      perl -p > "$ISABELLE_TARGET/${ISABELLE_NAME}.run" -e "s,{CLASSPATH},$LINUX_CLASSPATH,;"
-    chmod +x "$ISABELLE_TARGET/${ISABELLE_NAME}.run"
-
-    mv "$ISABELLE_TARGET/contrib/linux_app" "$TMP/."
-    cp "$TMP/linux_app/Isabelle" "$ISABELLE_TARGET/$ISABELLE_NAME"
-    ;;
-  macos)
-    purge_target 'contrib -name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
-    mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/."
-
-    perl -pi \
-      -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
-      -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
-      -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
-      -e "s,plugin-blacklist.MacOSX.jar=true,plugin-blacklist.MacOSX.jar=,g;" \
-      "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
-    ;;
-  windows)
-    purge_target 'contrib -name "x86*-linux" -o -name "x86*-darwin" -o -name "x86-cygwin"'
-
-    mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."
-
-    perl -pi \
-      -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
-      -e "s,foldPainter=.*,foldPainter=Square,g;" \
-      "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
-
-    (
-      init_component "$JEDIT_HOME"
-
-      echo -e "# Java runtime options\r"
-      eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
-      for ARG in "${JAVA_ARGS[@]}"
-      do
-        echo -e "$ARG\r"
-      done
-      echo -e "-Disabelle.jedit_server=${ISABELLE_NAME}\r"
-    ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.l4j.ini"
-
-    (
-      cd "$TMP"
-
-      APP_TEMPLATE="$ISABELLE_HOME/Admin/Windows/launch4j"
-
-      (
-        for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
-        do
-          ENTRY=$(echo "$ENTRY" | perl -p -e 's,/,\\\\,g;')
-          echo "    <cp>%EXEDIR%\\\\$ENTRY</cp>"
-        done
-      ) > exe_classpath
-      EXE_CLASSPATH="$(cat exe_classpath)"
-
-      perl -p \
-        -e "s,{OUTFILE},$ISABELLE_TARGET/${ISABELLE_NAME}.exe,g;" \
-        -e "s,{ICON},$APP_TEMPLATE/isabelle_transparent.ico,g;" \
-        -e "s,{SPLASH},$APP_TEMPLATE/isabelle.bmp,g;" \
-        -e "s,{CLASSPATH},$EXE_CLASSPATH,g;" \
-        -e "s,{ISABELLE_NAME},$ISABELLE_NAME,g;" \
-        "$APP_TEMPLATE/isabelle.xml" > isabelle.xml
-
-      "windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j" isabelle.xml
-
-      cp "$APP_TEMPLATE/manifest.xml" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe.manifest"
-    )
-
-    (
-      cd "$ISABELLE_TARGET"
-
-      cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" .
-
-      CYGWIN_MIRROR="$(cat contrib/cygwin/isabelle/cygwin_mirror)"
-      cat "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" | \
-        perl -p > "Cygwin-Setup.bat" -e "s,{MIRROR},$CYGWIN_MIRROR,;"
-      chmod +x "Cygwin-Setup.bat"
-
-      for NAME in postinstall rebaseall
-      do
-        cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" \
-          "contrib/cygwin/isabelle/."
-      done
-
-      if [ "$ISABELLE_PLATFORM_FAMILY" = macos ]; then
-        find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
-          -print0 > "contrib/cygwin/isabelle/executables"
-      else
-        find . -type f -not -name '*.exe' -not -name '*.dll' -executable \
-          -print0 > "contrib/cygwin/isabelle/executables"
-      fi
-
-      find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
-        > "contrib/cygwin/isabelle/symlinks"
-      find . -type l -exec rm "{}" ";"
-
-      touch "contrib/cygwin/isabelle/uninitialized"
-    )
-    ;;
-  *)
-    ;;
-esac
-
-
-# archive
-
-BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz"
-
-echo "packaging $(basename "$BUNDLE_ARCHIVE")"
-tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" || exit 2
-
-
-# platform-specific setup (outside archive)
-
-case "$PLATFORM_FAMILY" in
-  linux)
-    echo "application for $PLATFORM_FAMILY"
-    ln -s "${ISABELLE_NAME}_linux.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}_app.tar.gz"
-    ;;
-  macos)
-    echo "application for $PLATFORM_FAMILY"
-    (
-      cd "$TMP"
-
-      APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS"
-      APP="dmg/${ISABELLE_NAME}.app"
-
-      mkdir -p "dmg/.background"
-      cp "$APP_TEMPLATE/dmg/background.png" "dmg/.background/"
-      cp "$APP_TEMPLATE/dmg/DS_Store" "dmg/.DS_Store"
-      ln -s /Applications "dmg/."
-
-      for NAME in Java MacOS PlugIns Resources
-      do
-        mkdir -p "$APP/Contents/$NAME"
-      done
-
-      (
-        init_component "$JEDIT_HOME"
-
-        cat "$APP_TEMPLATE/Info.plist-part1"
-
-        declare -a OPTIONS=()
-        eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
-        for OPT in "${OPTIONS[@]}"
-        do
-          echo "<string>$OPT</string>"
-        done
-        echo "<string>-Disabelle.jedit_server={ISABELLE_NAME}</string>"
-        echo "<string>-Dapple.awt.application.name={ISABELLE_NAME}</string>"
-
-        cat "$APP_TEMPLATE/Info.plist-part2"
-      ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
-
-      for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}"
-      do
-        ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$APP/Contents/Java"
-      done
-
-      cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
-
-      ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk/x86_64-darwin" \
-        "$APP/Contents/PlugIns/bundled.jdk"
-
-      cp macos_app/JavaAppLauncher "$APP/Contents/MacOS/." && \
-        chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
-
-      mv "$ISABELLE_NAME" "$APP/Contents/Resources/."
-      ln -sf "../../Info.plist" "$APP/Contents/Resources/$ISABELLE_NAME/${ISABELLE_NAME}.plist"
-      ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
-
-      rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
-      tar -C dmg -czf "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" .
-
-      if [ -n "$REMOTE_MAC" ]
-      then
-        echo -n "$REMOTE_MAC: building dmg ..."
-        isabelle remote_dmg -V Isabelle "$REMOTE_MAC" \
-          "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" &&
-          echo " done"
-      fi
-    )
-    ;;
-  windows)
-    (
-      cd "$TMP"
-      rm -f "$TMP/${ISABELLE_NAME}.7z"
-      7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME"
-      [ -f "$TMP/${ISABELLE_NAME}.7z" ] || exit 2
-
-      echo "application for $PLATFORM_FAMILY"
-      (
-        cat "windows_app/7zsd_All_x64.sfx"
-        cat "$ISABELLE_HOME/Admin/Windows/Installer/sfx.txt" | \
-          perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;"
-        cat "$TMP/${ISABELLE_NAME}.7z"
-      ) > "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
-      chmod +x "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
-    )
-    ;;
-  *)
-    ;;
-esac
-
-
-# clean up
-rm -rf "$TMP"
--- a/src/Pure/Admin/build_release.scala	Tue Dec 04 16:11:52 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Wed Dec 05 19:42:40 2018 +0100
@@ -21,6 +21,7 @@
   }
 
   class Release private[Build_Release](
+    progress: Progress,
     val date: Date,
     val dist_name: String,
     val dist_dir: Path,
@@ -31,7 +32,10 @@
     val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
     val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
 
-    val other_isabelle_identifier: String = dist_name + "-build"
+    def other_isabelle(dir: Path): Other_Isabelle =
+      Other_Isabelle(dir + Path.explode(dist_name),
+        isabelle_identifier = dist_name + "-build",
+        progress = progress)
 
     def bundle_info(platform_family: String): Bundle_Info =
       platform_family match {
@@ -168,10 +172,17 @@
         } yield bundled(line)).toList))
   }
 
-  def get_bundled_components(dir: Path, platform: String): List[String] =
+  def get_bundled_components(dir: Path, platform: String): (List[String], String) =
   {
     val Bundled = new Bundled(platform)
-    for (Bundled(name) <- Components.read_components(dir)) yield name
+    val components =
+      for {
+        Bundled(name) <- Components.read_components(dir)
+        if !name.startsWith("jedit_build")
+      } yield name
+    val jdk_component =
+      components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
+    (components, jdk_component)
   }
 
   def activate_bundled_components(dir: Path, platform: String)
@@ -202,28 +213,6 @@
 
   /** build_release **/
 
-  def distribution_classpath(
-    components_base: Path,
-    isabelle_home: Path,
-    isabelle_classpath: String): List[Path] =
-  {
-    val base = isabelle_home.absolute
-    val contrib_base = components_base.absolute
-
-    Path.split(isabelle_classpath).map(path =>
-    {
-      val abs_path = path.absolute
-      File.relative_path(base, abs_path) match {
-        case Some(rel_path) => rel_path
-        case None =>
-          File.relative_path(contrib_base, abs_path) match {
-            case Some(rel_path) => Components.contrib() + rel_path
-            case None => error("Bad ISABELLE_CLASSPATH element: " + path)
-          }
-      }
-    }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
-  }
-
   private def execute(dir: Path, script: String): Unit =
     Isabelle_System.bash(script, cwd = dir.file).check
 
@@ -236,6 +225,7 @@
   private val default_platform_families = List("linux", "windows", "macos")
 
   def build_release(base_dir: Path,
+    options: Options,
     components_base: Option[Path] = None,
     progress: Progress = No_Progress,
     rev: String = "",
@@ -267,7 +257,7 @@
           case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
         }
 
-      new Release(date, dist_name, dist_dir, dist_version, ident)
+      new Release(progress, date, dist_name, dist_dir, dist_version, ident)
     }
 
 
@@ -320,13 +310,12 @@
 
       execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
 
+      record_bundled_components(release.isabelle_dir)
+
 
       /* build tools and documentation */
 
-      val other_isabelle =
-        Other_Isabelle(release.isabelle_dir,
-          isabelle_identifier = release.other_isabelle_identifier,
-          progress = progress)
+      val other_isabelle = release.other_isabelle(release.dist_dir)
 
       other_isabelle.init_settings(
         other_isabelle.init_components(base = components_base, catalogs = List("main")))
@@ -406,13 +395,262 @@
       if (bundle_archive.is_file)
         progress.echo_warning("Application bundle already exists: " + bundle_archive)
       else {
-        progress.echo(
-          "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive)
-        progress.bash(
-          "isabelle makedist_bundle " + File.bash_path(release.isabelle_archive) +
-            " " + Bash.string(bundle_info.platform_family) +
-            (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
-          echo = true).check
+        val isabelle_name = release.dist_name
+        val platform = bundle_info.platform_family
+
+        progress.echo("\nApplication bundle for " + platform + ": " + bundle_archive)
+
+        Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
+        {
+          // release archive
+
+          execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
+          val other_isabelle = release.other_isabelle(tmp_dir)
+          val isabelle_target = other_isabelle.isabelle_home
+
+
+          // bundled components
+
+          progress.echo("Bundled components:")
+
+          val contrib_dir = Components.contrib(isabelle_target)
+
+          val (components, jdk_component) = get_bundled_components(isabelle_target, platform)
+
+          Components.resolve(other_isabelle.components_base(components_base),
+            components, target_dir = Some(contrib_dir), progress = progress)
+
+          Components.purge(contrib_dir, platform)
+
+          activate_bundled_components(isabelle_target, platform)
+
+
+          // Java parameters
+
+          val java_options_title = "# Java runtime options"
+          val java_options: List[String] =
+            (for {
+              variable <-
+                List(
+                  "ISABELLE_JAVA_SYSTEM_OPTIONS",
+                  "JEDIT_JAVA_SYSTEM_OPTIONS",
+                  "JEDIT_JAVA_OPTIONS")
+              opt <- Word.explode(other_isabelle.getenv(variable))
+            } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
+
+          val classpath: List[Path] =
+          {
+            val base = isabelle_target.absolute
+            Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
+            {
+              val abs_path = path.absolute
+              File.relative_path(base, abs_path) match {
+                case Some(rel_path) => rel_path
+                case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
+              }
+            }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
+          }
+
+          val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
+
+
+          // platform-specific setup (inside archive)
+
+          if (platform == "linux") {
+            File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
+              terminate_lines(java_options_title :: java_options))
+
+            val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
+            File.write(isabelle_run,
+              File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
+                .replaceAllLiterally("{CLASSPATH}",
+                  classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
+                .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
+            Isabelle_System.bash("chmod +x " + File.bash_path(isabelle_run)).check
+
+            val linux_app = isabelle_target + Path.explode("contrib/linux_app")
+            File.move(linux_app + Path.explode("Isabelle"),
+              isabelle_target + Path.explode(isabelle_name))
+            Isabelle_System.rm_tree(linux_app)
+          }
+          else if (platform == "macos") {
+            File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
+            File.write(isabelle_target + jedit_props,
+              File.read(isabelle_target + jedit_props)
+                .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
+                .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
+                .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
+                .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
+          }
+          else if (platform == "windows") {
+            val app_template = Path.explode("~~/Admin/Windows/launch4j")
+            val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
+
+            File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
+
+            File.write(isabelle_target + jedit_props,
+              File.read(isabelle_target + jedit_props)
+                .replaceAll("lookAndFeel=.*",
+                  "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
+                .replaceAll("foldPainter=.*", "foldPainter=Square"))
+
+            File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
+              (java_options_title :: java_options).map(_ + "\r\n").mkString)
+
+            val isabelle_xml = Path.explode("isabelle.xml")
+            val isabelle_exe = Path.explode(isabelle_name + ".exe")
+
+            File.write(tmp_dir + isabelle_xml,
+              File.read(app_template + isabelle_xml)
+                .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+                .replaceAllLiterally("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
+                .replaceAllLiterally("{ICON}",
+                  File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
+                .replaceAllLiterally("{SPLASH}",
+                  File.platform_path(app_template + Path.explode("isabelle.bmp")))
+                .replaceAllLiterally("{CLASSPATH}",
+                  cat_lines(classpath.map(cp =>
+                    "    <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
+                .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
+
+            Isabelle_System.bash(
+              "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml",
+              cwd = tmp_dir.file).check
+
+            File.copy(app_template + Path.explode("manifest.xml"),
+              isabelle_target + isabelle_exe.ext("manifest"))
+
+
+            File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
+
+            val cygwin_mirror =
+              File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
+
+            val cygwin_bat = Path.explode("Cygwin-Setup.bat")
+            File.write(isabelle_target + cygwin_bat,
+              File.read(cygwin_template + cygwin_bat)
+                .replaceAllLiterally("{MIRROR}", cygwin_mirror))
+
+            Isabelle_System.bash("chmod +x " + File.bash_path(isabelle_target + cygwin_bat)).check
+
+            for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
+              val path = Path.explode(name)
+              File.copy(cygwin_template + path,
+                isabelle_target + Path.explode("contrib/cygwin") + path)
+            }
+
+            Isabelle_System.bash("""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
+              (if (Platform.is_macos) "-perm +100" else "-executable") +
+              " -print0 > contrib/cygwin/isabelle/executables",
+              cwd = isabelle_target.file).check
+
+            Isabelle_System.bash("""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
+              """> contrib/cygwin/isabelle/symlinks""",
+              cwd = isabelle_target.file).check
+
+            Isabelle_System.bash("""find . -type l -exec rm "{}" ";" """,
+              cwd = isabelle_target.file).check
+
+            File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
+          }
+
+
+          // archive
+
+          val archive_name = isabelle_name + "_" + platform + ".tar.gz"
+          progress.echo("Packaging " + archive_name)
+          execute_tar(tmp_dir,
+            "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+            Bash.string(isabelle_name))
+
+
+          // platform-specific application (outside archive)
+
+          progress.echo("Application for " + platform)
+
+          if (platform == "linux") {
+            Isabelle_System.bash(
+              "ln -s " + Bash.string(isabelle_name + "_linux.tar.gz") + " " +
+              File.bash_path(release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"))).check
+          }
+          else if (platform == "macos") {
+            val dmg_dir = tmp_dir + Path.explode("macos_app/dmg")
+            val app_dir = dmg_dir + Path.explode(isabelle_name + ".app")
+            File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir)
+
+            val app_contents = app_dir + Path.explode("Contents")
+            val app_resources = app_contents + Path.explode("Resources")
+            File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
+
+            File.write(app_contents + Path.explode("Info.plist"),
+              File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
+                .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+                .replaceAllLiterally("{JAVA_OPTIONS}",
+                  terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
+
+            for (cp <- classpath) {
+              Isabelle_System.bash(
+                "ln -sf " +
+                Bash.string("../Resources/" + isabelle_name + "/") + File.bash_path(cp) + " " +
+                File.bash_path(app_contents + Path.explode("Java"))).check
+            }
+
+            Isabelle_System.bash("ln -sf ../Resources/" + Bash.string(isabelle_name) +
+              "/contrib/" + Bash.string(jdk_component) + "/x86_64-darwin " +
+              File.bash_path(app_contents + Path.explode("PlugIns/bundled.jdk"))).check
+
+            Isabelle_System.bash("ln -sf ../../Info.plist " +
+              File.bash_path(app_resources + Path.explode(isabelle_name) +
+                Path.explode(isabelle_name + ".plist"))).check
+            Isabelle_System.bash("ln -sf Contents/Resources/" + Bash.string(isabelle_name) + " " +
+              File.bash_path(app_dir) + "/Isabelle").check
+
+            val dmg = Path.explode(isabelle_name + ".dmg")
+            (release.dist_dir + dmg).file.delete
+
+            val dmg_archive = Path.explode(isabelle_name + "_dmg.tar.gz")
+            execute_tar(dmg_dir, "-czf " + File.bash_path(release.dist_dir + dmg_archive) + " .")
+
+            remote_mac match {
+              case SSH.Target(user, host) =>
+                progress.echo("Building dmg on " + quote(host) + " ...")
+                using(SSH.open_session(options, host = host, user = user))(ssh =>
+                {
+                  ssh.with_tmp_dir(remote_dir =>
+                  {
+                    val cd = "cd " + ssh.bash_path(remote_dir) + "; "
+                    ssh.write_file(remote_dir + dmg_archive, release.dist_dir + dmg_archive)
+                    ssh.execute(
+                      cd + "mkdir root && tar -C root -xzf " + ssh.bash_path(dmg_archive)).check
+                    ssh.execute(
+                      cd + "hdiutil create -srcfolder root -volname Isabelle " +
+                      ssh.bash_path(dmg)).check
+                    ssh.read_file(remote_dir + dmg, release.dist_dir + dmg)
+                  })
+                })
+              case _ =>
+            }
+          }
+          else if (platform == "windows") {
+            val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z")
+            exe_archive.file.delete
+
+            Isabelle_System.bash("7z -y -bd a " + File.bash_path(exe_archive) + " " +
+              Bash.string(isabelle_name), cwd = tmp_dir.file).check
+            if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
+
+            val isabelle_exe = Path.explode(isabelle_name + ".exe")
+            val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
+            val sfx_txt =
+              File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
+                replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+
+            Bytes.write(release.dist_dir + isabelle_exe,
+              Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
+
+            Isabelle_System.bash("chmod +x " + (release.dist_dir + isabelle_exe)).check
+          }
+        })
       }
     }
 
@@ -452,14 +690,12 @@
       else {
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
-            val name = release.dist_name
             val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
-            val bundle = release.dist_dir + Path.explode(name + "_" + platform + ".tar.gz")
+            val bundle =
+              release.dist_dir + Path.explode(release.dist_name + "_" + platform + ".tar.gz")
             execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
 
-            val other_isabelle =
-              Other_Isabelle(tmp_dir + Path.explode(name),
-                isabelle_identifier = release.other_isabelle_identifier, progress = progress)
+            val other_isabelle = release.other_isabelle(tmp_dir)
 
             Isabelle_System.mkdirs(other_isabelle.etc)
             File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
@@ -469,11 +705,11 @@
                 " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
             other_isabelle.isabelle_home_user.file.delete
 
-            execute(tmp_dir, "chmod -R a+r " + Bash.string(name))
-            execute(tmp_dir, "chmod -R g=o " + Bash.string(name))
+            execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
+            execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
             execute_tar(tmp_dir,
               tar_options + " -czf " + File.bash_path(release.isabelle_library_archive) +
-              " " + Bash.string(name + "/browser_info"))
+              " " + Bash.string(release.dist_name + "/browser_info"))
           })
       }
     }
@@ -496,6 +732,7 @@
       var website: Option[Path] = None
       var parallel_jobs = 1
       var build_library = false
+      var options = Options.init()
       var platform_families = default_platform_families
       var rev = ""
 
@@ -511,6 +748,7 @@
     -W WEBSITE   produce minimal website in given directory
     -j INT       maximum number of parallel jobs (default 1)
     -l           build library
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
     -r REV       Mercurial changeset id (default: RELEASE or tip)
 
@@ -524,6 +762,7 @@
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
+        "o:" -> (arg => options = options + arg),
         "p:" -> (arg => platform_families = space_explode(',', arg)),
         "r:" -> (arg => rev = arg))
 
@@ -532,8 +771,8 @@
 
       val progress = new Console_Progress()
 
-      build_release(Path.explode(base_dir), components_base = components_base, progress = progress,
-        rev = rev, afp_rev = afp_rev, official_release = official_release,
+      build_release(Path.explode(base_dir), options, components_base = components_base,
+        progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
         proper_release_name = proper_release_name, website = website,
         platform_families =
           if (platform_families.isEmpty) default_platform_families
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Dec 04 16:11:52 2018 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Dec 05 19:42:40 2018 +0100
@@ -75,7 +75,7 @@
   val build_release =
     Logger_Task("build_release", logger =>
       {
-        Isabelle_Devel.release_snapshot(
+        Isabelle_Devel.release_snapshot(logger.options,
           rev = get_rev(), afp_rev = get_afp_rev(), remote_mac = "macbroy30")
       })
 
--- a/src/Pure/Admin/isabelle_devel.scala	Tue Dec 04 16:11:52 2018 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala	Wed Dec 05 19:42:40 2018 +0100
@@ -51,6 +51,7 @@
   /* release snapshot */
 
   def release_snapshot(
+    options: Options,
     rev: String = "",
     afp_rev: String = "",
     parallel_jobs: Int = 1,
@@ -60,7 +61,7 @@
       {
         Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
           website_dir =>
-            Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
+            Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev,
               parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir)))
       })
   }
--- a/src/Pure/Admin/other_isabelle.scala	Tue Dec 04 16:11:52 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Wed Dec 05 19:42:40 2018 +0100
@@ -68,12 +68,15 @@
 
   /* components */
 
+  def components_base(base: Option[Path]): Path =
+    base getOrElse Components.contrib(isabelle_home_user.absolute.dir)
+
   def init_components(
     base: Option[Path] = None,
     catalogs: List[String] = Nil,
     components: List[String] = Nil): List[String] =
   {
-    val base_dir = base getOrElse Components.contrib(isabelle_home_user.absolute.dir)
+    val base_dir = components_base(base)
     val dir = Components.admin(isabelle_home.absolute)
     catalogs.map(name =>
       "init_components " + File.bash_path(base_dir) + " " + File.bash_path(dir + Path.basic(name))) :::
--- a/src/Pure/Admin/remote_dmg.scala	Tue Dec 04 16:11:52 2018 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-/*  Title:      Pure/Admin/remote_dmg.scala
-    Author:     Makarius
-
-Build dmg on remote Mac OS X system.
-*/
-
-package isabelle
-
-
-object Remote_DMG
-{
-  def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
-  {
-    ssh.with_tmp_dir(remote_dir =>
-      {
-        val cd = "cd " + ssh.bash_path(remote_dir) + "; "
-
-        ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
-        ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
-        ssh.execute(
-          cd + "hdiutil create -srcfolder root" +
-            (if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) +
-            " dmg.dmg").check
-        ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
-      })
-  }
-
-
-  /* Isabelle tool wrapper */
-
-  val isabelle_tool =
-    Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args =>
-    {
-      Command_Line.tool0 {
-        var port = 0
-        var volume_name = ""
-
-        val getopts = Getopts("""
-Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE
-
-  Options are:
-    -p PORT      alternative SSH port
-    -V NAME      specify volume name
-
-  Turn the contents of a tar.gz file into a dmg file -- produced on a remote
-  Mac OS X system.
-""",
-          "p:" -> (arg => port = Value.Int.parse(arg)),
-          "V:" -> (arg => volume_name = arg))
-
-        val more_args = getopts(args)
-        val (user, host, tar_gz_file, dmg_file) =
-          more_args match {
-            case List(SSH.Target(user, host), tar_gz_file, dmg_file) =>
-              (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file))
-            case _ => getopts.usage()
-          }
-
-        val options = Options.init()
-        using(SSH.open_session(options, host = host, user = user, port = port))(
-          remote_dmg(_, tar_gz_file, dmg_file, volume_name))
-      }
-    })
-}
--- a/src/Pure/System/components.scala	Tue Dec 04 16:11:52 2018 +0100
+++ b/src/Pure/System/components.scala	Wed Dec 05 19:42:40 2018 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import java.io.{File => JFile}
+
+
 object Components
 {
   /* component collections */
@@ -16,20 +19,43 @@
   def contrib(dir: Path = Path.current, name: String = ""): Path =
     dir + Path.explode("contrib") + Path.explode(name)
 
-  def download(dir: Path, names: List[String], progress: Progress = No_Progress)
+  def resolve(base_dir: Path, names: List[String],
+    target_dir: Option[Path] = None,
+    progress: Progress = No_Progress)
   {
-    Isabelle_System.mkdirs(dir)
+    Isabelle_System.mkdirs(base_dir)
     for (name <- names) {
-      val archive = name + ".tar.gz"
-      val target = dir + Path.explode(archive)
-      if (!target.is_file) {
-        val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive
-        progress.echo("Getting " + quote(remote))
-        Bytes.write(target, Url.read_bytes(Url(remote)))
+      val archive_name = name + ".tar.gz"
+      val archive = base_dir + Path.explode(archive_name)
+      if (!archive.is_file) {
+        val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
+        progress.echo("Getting " + remote)
+        Bytes.write(archive, Url.read_bytes(Url(remote)))
       }
+      progress.echo("Unpacking " + archive_name)
+      Isabelle_System.gnutar(
+        "-C " + File.bash_path(target_dir getOrElse base_dir) +
+        " -xzf " + File.bash_path(archive)).check
     }
   }
 
+  def purge(dir: Path, platform: String)
+  {
+    def purge_platforms(platforms: String*): Set[String] =
+      platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
+    val purge_set =
+      platform match {
+        case "linux" => purge_platforms("darwin", "cygwin", "windows")
+        case "windows" => purge_platforms("linux", "darwin")
+        case "macos" => purge_platforms("linux", "cygwin", "windows")
+        case _ => error("Bad platform: " + quote(platform))
+      }
+
+    File.find_files(dir.file,
+      (file: JFile) => file.isDirectory && purge_set(file.getName),
+      include_dirs = true).foreach(Isabelle_System.rm_tree)
+  }
+
 
   /* component directory content */
 
--- a/src/Pure/System/isabelle_tool.scala	Tue Dec 04 16:11:52 2018 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Wed Dec 05 19:42:40 2018 +0100
@@ -172,5 +172,4 @@
   Build_PolyML.isabelle_tool2,
   Build_Status.isabelle_tool,
   Check_Sources.isabelle_tool,
-  Remote_DMG.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool)
--- a/src/Pure/build-jars	Tue Dec 04 16:11:52 2018 +0100
+++ b/src/Pure/build-jars	Wed Dec 05 19:42:40 2018 +0100
@@ -25,7 +25,6 @@
   Admin/isabelle_devel.scala
   Admin/jenkins.scala
   Admin/other_isabelle.scala
-  Admin/remote_dmg.scala
   Concurrent/consumer_thread.scala
   Concurrent/counter.scala
   Concurrent/event_timer.scala