--- a/src/Pure/GUI/gui.scala Mon Dec 21 21:56:20 2020 +0100
+++ b/src/Pure/GUI/gui.scala Mon Dec 21 22:03:39 2020 +0100
@@ -35,13 +35,13 @@
def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
+ def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
+
def is_macos_laf(): Boolean =
- Platform.is_macos &&
- UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
+ Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
def is_windows_laf(): Boolean =
- Platform.is_windows &&
- UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
+ Platform.is_windows && UIManager.getSystemLookAndFeelClassName() == current_laf()
/* plain focus traversal, notably for text fields */