equal
deleted
inserted
replaced
32 def get_laf(): String = |
32 def get_laf(): String = |
33 find_laf(System.getProperty("isabelle.laf")) getOrElse { |
33 find_laf(System.getProperty("isabelle.laf")) getOrElse { |
34 if (Platform.is_windows || Platform.is_macos) |
34 if (Platform.is_windows || Platform.is_macos) |
35 UIManager.getSystemLookAndFeelClassName() |
35 UIManager.getSystemLookAndFeelClassName() |
36 else |
36 else |
37 find_laf("Nimbus") getOrElse |
37 UIManager.getCrossPlatformLookAndFeelClassName() |
38 UIManager.getCrossPlatformLookAndFeelClassName() |
|
39 } |
38 } |
40 |
39 |
41 def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) |
40 def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) |
42 |
41 |
43 def is_macos_laf(): Boolean = |
42 def is_macos_laf(): Boolean = |