src/Pure/GUI/gui.scala
changeset 72975 315f9b4f9e7a
parent 72974 3afd293347cc
child 73037 473509b160d9
equal deleted inserted replaced
72974:3afd293347cc 72975:315f9b4f9e7a
    33         UIManager.getCrossPlatformLookAndFeelClassName()
    33         UIManager.getCrossPlatformLookAndFeelClassName()
    34     }
    34     }
    35 
    35 
    36   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
    36   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
    37 
    37 
       
    38   def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
       
    39 
    38   def is_macos_laf(): Boolean =
    40   def is_macos_laf(): Boolean =
    39     Platform.is_macos &&
    41     Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
    40     UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
       
    41 
    42 
    42   def is_windows_laf(): Boolean =
    43   def is_windows_laf(): Boolean =
    43     Platform.is_windows &&
    44     Platform.is_windows && UIManager.getSystemLookAndFeelClassName() == current_laf()
    44     UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
       
    45 
    45 
    46 
    46 
    47   /* plain focus traversal, notably for text fields */
    47   /* plain focus traversal, notably for text fields */
    48 
    48 
    49   def plain_focus_traversal(component: Component)
    49   def plain_focus_traversal(component: Component)