# HG changeset patch # User wenzelm # Date 1611061471 -3600 # Node ID 31fbde3baa97b14b6857c91edd7ebcd1f817af40 # Parent aeba7bb4f4d4167e7e2d0d697c4ae37b6fa6d8cb more systematic java-gui-setup, also for "isabelle jedit" command-line tool; diff -r aeba7bb4f4d4 -r 31fbde3baa97 lib/scripts/java-gui-setup --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/java-gui-setup Tue Jan 19 14:04:31 2021 +0100 @@ -0,0 +1,11 @@ +#!/usr/bin/env bash +# +# java-gui-setup --- platform-specific setup for Java/Swing GUI applications + +if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ] +then + JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" + JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" + defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || + defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null +fi diff -r aeba7bb4f4d4 -r 31fbde3baa97 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Tue Jan 19 13:48:53 2021 +0100 +++ b/src/Pure/Admin/build_release.scala Tue Jan 19 14:04:31 2021 +0100 @@ -287,12 +287,7 @@ declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options")) -if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then - JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" - JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" - defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || - defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null -fi +"$ISABELLE_HOME/lib/scripts/java-gui-setup" exec "$ISABELLE_JDK_HOME/bin/java" \ "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ diff -r aeba7bb4f4d4 -r 31fbde3baa97 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Jan 19 13:48:53 2021 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Jan 19 14:04:31 2021 +0100 @@ -408,6 +408,8 @@ if [ "$BUILD_ONLY" = false ] then + "$ISABELLE_HOME/lib/scripts/java-gui-setup" + export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"