# HG changeset patch # User wenzelm # Date 1749820696 -7200 # Node ID a3e7732b03936874c2e74df965dfa6ef94c16c9b # Parent c0f166b39a3af71993a5dd1a6959958dab627678 more robust GUI setup via Java, instead of shell script; support for automatic / approximative GDK_SCALE for Linux; diff -r c0f166b39a3a -r a3e7732b0393 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Jun 12 16:54:28 2025 +0200 +++ b/Admin/components/components.sha1 Fri Jun 13 15:18:16 2025 +0200 @@ -196,6 +196,7 @@ f582c621471583d06e00007c6acc01376c7395af isabelle_setup-20230206.tar.gz d30109fe63cec35c31cee9ffd17ae3a13c1e6a33 isabelle_setup-20230922.tar.gz cd92c141883f0f6a18adceb885316c8b6119e648 isabelle_setup-20240327.tar.gz +ed96100db1c7fd0beee0c93929609cab42e952b8 isabelle_setup-20250613.tar.gz f23037b322b968c61350f9ec9995a4f397e6c71c javamail-1.4.7.tar.gz 18e6b60ceb98e327fbf14e52f4613dd5b0483d2f javamail-20240109.tar.gz dc826bc0d715cd4190d1bb2e7122321eea5355de javamail-20250122.tar.gz diff -r c0f166b39a3a -r a3e7732b0393 Admin/components/main --- a/Admin/components/main Thu Jun 12 16:54:28 2025 +0200 +++ b/Admin/components/main Fri Jun 13 15:18:16 2025 +0200 @@ -12,7 +12,7 @@ flatlaf-3.6-2 foiltex-2.1.4b isabelle_fonts-20241227 -isabelle_setup-20240327 +isabelle_setup-20250613 javamail-20250122 jdk-21.0.6 jedit-20250521 diff -r c0f166b39a3a -r a3e7732b0393 NEWS --- a/NEWS Thu Jun 12 16:54:28 2025 +0200 +++ b/NEWS Fri Jun 13 15:18:16 2025 +0200 @@ -44,6 +44,12 @@ Dark" imitate original macOS more closely. This is the default for the bundled application on macOS. +* Automatic GUI scaling on Linux, based on global GDK_SCALE for Java. +This is only an approximation: an integer factor that applies uniformly +to all displays. In contrast, Windows and macOS work with accurate GUI +scaling for each individual display, based on operating system settings +and FlatLaf defaults. + * GUI rendering of the gutter is now more accurate, using scaled icons to fit precisely into the available space. diff -r c0f166b39a3a -r a3e7732b0393 lib/scripts/java-gui-setup --- a/lib/scripts/java-gui-setup Thu Jun 12 16:54:28 2025 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -#!/usr/bin/env bash -# -# java-gui-setup --- platform-specific setup for Java/Swing GUI applications - -case "$ISABELLE_PLATFORM_FAMILY" in - macos*) - 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 - ;; -esac diff -r c0f166b39a3a -r a3e7732b0393 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Thu Jun 12 16:54:28 2025 +0200 +++ b/src/Pure/Admin/build_release.scala Fri Jun 13 15:18:16 2025 +0200 @@ -306,7 +306,7 @@ declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options")) -"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup" +eval $(isabelle java isabelle.setup.Setup gui_setup) exec "$ISABELLE_JDK_HOME/bin/java" \ "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ @@ -665,19 +665,6 @@ platform match { case Platform.Family.linux_arm | Platform.Family.linux => - File.change(isabelle_target + jedit_options) { - _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24") - } - - File.change(isabelle_target + jedit_props) { - _.replaceAll("console.fontsize=.*", "console.fontsize=18") - .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") - .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") - .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") - .replaceAll("view.fontsize=.*", "view.fontsize=24") - .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16") - } - make_isabelle_options( isabelle_target + Path.explode("Isabelle.options"), java_options) diff -r c0f166b39a3a -r a3e7732b0393 src/Pure/System/platform.scala --- a/src/Pure/System/platform.scala Thu Jun 12 16:54:28 2025 +0200 +++ b/src/Pure/System/platform.scala Fri Jun 13 15:18:16 2025 +0200 @@ -11,8 +11,8 @@ /* platform family */ val is_windows: Boolean = isabelle.setup.Environment.is_windows() - val is_linux: Boolean = System.getProperty("os.name", "") == "Linux" - val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X" + val is_linux: Boolean = isabelle.setup.Environment.is_linux() + val is_macos: Boolean = isabelle.setup.Environment.is_macos() val is_unix: Boolean = is_linux || is_macos def is_arm: Boolean = cpu_arch.startsWith("arm") diff -r c0f166b39a3a -r a3e7732b0393 src/Tools/Setup/etc/build.props --- a/src/Tools/Setup/etc/build.props Thu Jun 12 16:54:28 2025 +0200 +++ b/src/Tools/Setup/etc/build.props Fri Jun 13 15:18:16 2025 +0200 @@ -4,5 +4,6 @@ src/Build.java \ src/Environment.java \ src/Exn.java \ + src/GUI_Setup.java \ src/Library.java \ src/Setup.java diff -r c0f166b39a3a -r a3e7732b0393 src/Tools/Setup/src/Environment.java --- a/src/Tools/Setup/src/Environment.java Thu Jun 12 16:54:28 2025 +0200 +++ b/src/Tools/Setup/src/Environment.java Fri Jun 13 15:18:16 2025 +0200 @@ -30,6 +30,8 @@ { return System.getProperty("os.name", "").startsWith("Windows"); } + public static Boolean is_linux() { return System.getProperty("os.name", "").equals("Linux"); } + public static Boolean is_macos() { return System.getProperty("os.name", "").equals("Mac OS X"); } diff -r c0f166b39a3a -r a3e7732b0393 src/Tools/Setup/src/GUI_Setup.java --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Setup/src/GUI_Setup.java Fri Jun 13 15:18:16 2025 +0200 @@ -0,0 +1,43 @@ +/* Title: Tools/Setup/src/GUI_Setup.scala + Author: Makarius + +Platform-specific setup for Java/Swing GUI applications. +*/ + +package isabelle.setup; + +import java.util.List; + +import com.formdev.flatlaf.FlatLightLaf; +import com.formdev.flatlaf.util.UIScale; + + +public class GUI_Setup +{ + public static String gui_setup() + { + String msg = ""; + + if (Environment.is_linux()) { + if (FlatLightLaf.setup()) { + int scale = (int) UIScale.getUserScaleFactor(); + if (scale > 1) { msg = "export GDK_SCALE=" + scale; } + } + } + else if (Environment.is_macos()) { + String java_domain = "com.azul.zulu." + System.getProperty("java.version") + ".java"; + if (!apple_tabbing_mode("read", java_domain)) { + apple_tabbing_mode("write", java_domain); + } + } + + return msg; + } + + public static boolean apple_tabbing_mode(String op, String domain) + { + List cmd = java.util.List.of("defaults", op, domain, "AppleWindowTabbingMode"); + try { return Environment.exec_process(cmd, null, null, false).ok(); } + catch (Exception e) { return false; } + } +} diff -r c0f166b39a3a -r a3e7732b0393 src/Tools/Setup/src/Setup.java --- a/src/Tools/Setup/src/Setup.java Thu Jun 12 16:54:28 2025 +0200 +++ b/src/Tools/Setup/src/Setup.java Fri Jun 13 15:18:16 2025 +0200 @@ -48,6 +48,11 @@ check_args(n == 1); echo(Environment.join_standard_paths(Build.classpath())); break; + case "gui_setup": + check_args(n == 1); + String msg = GUI_Setup.gui_setup(); + if (msg != null && !msg.isEmpty()) { echo(msg); } + break; case "services": check_args(n == 1); for (String s : Build.services()) { echo(s); } diff -r c0f166b39a3a -r a3e7732b0393 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Jun 12 16:54:28 2025 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jun 13 15:18:16 2025 +0200 @@ -168,7 +168,7 @@ if [ "$BUILD_ONLY" = false ] then - "$ISABELLE_HOME/lib/scripts/java-gui-setup" + eval $(isabelle java isabelle.setup.Setup gui_setup) export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_ISABELLE_OPTIONS JEDIT_BUILD_MODE